Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Module docstring

{"# Topology and uniform structure of uniform convergence

This files endows α → β with the topologies / uniform structures of - uniform convergence on α - uniform convergence on a specified family 𝔖 of sets of α, also called 𝔖-convergence

Since α → β is already endowed with the topologies and uniform structures of pointwise convergence, we introduce type aliases UniformFun α β (denoted α →ᵤ β) and UniformOnFun α β 𝔖 (denoted α →ᵤ[𝔖] β) and we actually endow these with the structures of uniform and 𝔖-convergence respectively.

Usual examples of the second construction include : - the topology of compact convergence, when 𝔖 is the set of compacts of α - the strong topology on the dual of a topological vector space (TVS) E, when 𝔖 is the set of Von Neumann bounded subsets of E - the weak-* topology on the dual of a TVS E, when 𝔖 is the set of singletons of E.

This file contains a lot of technical facts, so it is heavily commented, proofs included!

Main definitions

UniformFun.gen: basis sets for the uniformity of uniform convergence. These are sets of the form S(V) := {(f, g) | ∀ x : α, (f x, g x) ∈ V} for some V : Set (β × β)
UniformFun.uniformSpace: uniform structure of uniform convergence. This is the UniformSpace on α →ᵤ β whose uniformity is generated by the sets S(V) for V ∈ 𝓤 β. We will denote this uniform space as 𝒰(α, β, uβ), both in the comments and as a local notation in the Lean code, where uβ is the uniform space structure on β. This is declared as an instance on α →ᵤ β.
UniformOnFun.uniformSpace: uniform structure of 𝔖-convergence, where 𝔖 : Set (Set α). This is the infimum, for S ∈ 𝔖, of the pullback of 𝒰 S β by the map of restriction to S. We will denote it 𝒱(α, β, 𝔖, uβ), where uβ is the uniform space structure on β. This is declared as an instance on α →ᵤ[𝔖] β.

Main statements

Basic properties

UniformFun.uniformContinuous_eval: evaluation is uniformly continuous on α →ᵤ β.
UniformFun.t2Space: the topology of uniform convergence on α →ᵤ β is T₂ if β is T₂.
UniformFun.tendsto_iff_tendstoUniformly: 𝒰(α, β, uβ) is indeed the uniform structure of uniform convergence
UniformOnFun.uniformContinuous_eval_of_mem: evaluation at a point contained in a set of 𝔖 is uniformly continuous on α →ᵤ[𝔖] β
UniformOnFun.t2Space_of_covering: the topology of 𝔖-convergence on α →ᵤ[𝔖] β is T₂ if β is T₂ and 𝔖 covers α
UniformOnFun.tendsto_iff_tendstoUniformlyOn: 𝒱(α, β, 𝔖 uβ) is indeed the uniform structure of 𝔖-convergence

Functoriality and compatibility with product of uniform spaces

In order to avoid the need for filter bases as much as possible when using these definitions, we develop an extensive API for manipulating these structures abstractly. As usual in the topology section of mathlib, we first state results about the complete lattices of UniformSpaces on fixed types, and then we use these to deduce categorical-like results about maps between two uniform spaces.

We only describe these in the harder case of 𝔖-convergence, as the names of the corresponding results for uniform convergence can easily be guessed.

Order statements

UniformOnFun.mono: let u₁, u₂ be two uniform structures on γ and 𝔖₁ 𝔖₂ : Set (Set α). If u₁ ≤ u₂ and 𝔖₂ ⊆ 𝔖₁ then 𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂).
UniformOnFun.iInf_eq: if u is a family of uniform structures on γ, then 𝒱(α, γ, 𝔖, (⨅ i, u i)) = ⨅ i, 𝒱(α, γ, 𝔖, u i).
UniformOnFun.comap_eq: if u is a uniform structures on β and f : γ → β, then 𝒱(α, γ, 𝔖, comap f u) = comap (fun g ↦ f ∘ g) 𝒱(α, γ, 𝔖, u₁).

An interesting note about these statements is that they are proved without ever unfolding the basis definition of the uniform structure of uniform convergence! Instead, we build a (not very interesting) Galois connection UniformFun.gc and then rely on the Galois connection API to do most of the work.

Morphism statements (unbundled)

UniformOnFun.postcomp_uniformContinuous: if f : γ → β is uniformly continuous, then (fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β) is uniformly continuous.
UniformOnFun.postcomp_isUniformInducing: if f : γ → β is a uniform inducing, then (fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β) is a uniform inducing.
UniformOnFun.precomp_uniformContinuous: let f : γ → α, 𝔖 : Set (Set α), 𝔗 : Set (Set γ), and assume that ∀ T ∈ 𝔗, f '' T ∈ 𝔖. Then, the function (fun g ↦ g ∘ f) : (α →ᵤ[𝔖] β) → (γ →ᵤ[𝔗] β) is uniformly continuous.

Isomorphism statements (bundled)

UniformOnFun.congrRight: turn a uniform isomorphism γ ≃ᵤ β into a uniform isomorphism (α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β) by post-composing.
UniformOnFun.congrLeft: turn a bijection e : γ ≃ α such that we have both ∀ T ∈ 𝔗, e '' T ∈ 𝔖 and ∀ S ∈ 𝔖, e ⁻¹' S ∈ 𝔗 into a uniform isomorphism (γ →ᵤ[𝔗] β) ≃ᵤ (α →ᵤ[𝔖] β) by pre-composing.
UniformOnFun.uniformEquivPiComm: the natural bijection between α → Π i, δ i and Π i, α → δ i, upgraded to a uniform isomorphism between α →ᵤ[𝔖] (Π i, δ i) and Π i, α →ᵤ[𝔖] δ i.

Important use cases

If G is a uniform group, then α →ᵤ[𝔖] G is a uniform group: since (/) : G × G → G is uniformly continuous, UniformOnFun.postcomp_uniformContinuous tells us that ((/) ∘ —) : (α →ᵤ[𝔖] G × G) → (α →ᵤ[𝔖] G) is uniformly continuous. By precomposing with UniformOnFun.uniformEquivProdArrow, this gives that (/) : (α →ᵤ[𝔖] G) × (α →ᵤ[𝔖] G) → (α →ᵤ[𝔖] G) is also uniformly continuous
The transpose of a continuous linear map is continuous for the strong topologies: since continuous linear maps are uniformly continuous and map bounded sets to bounded sets, this is just a special case of UniformOnFun.precomp_uniformContinuous.

TODO

Show that the uniform structure of 𝔖-convergence is exactly the structure of 𝔖'-convergence, where 𝔖' is the noncovering bornology (i.e not what Bornology currently refers to in mathlib) generated by 𝔖.

References

[N. Bourbaki, General Topology, Chapter X][bourbaki1966]

Tags

uniform convergence "}

UniformFun definition

(α β : Type*)

Full source

/-- The type of functions from `α` to `β` equipped with the uniform structure and topology of
uniform convergence. We denote it `α →ᵤ β`. -/
def UniformFun (α β : Type*) :=
  α → β

Uniform convergence function space

Informal description

The type of functions from a type $\alpha$ to a uniform space $\beta$, equipped with the uniform structure and topology of uniform convergence. This is denoted by $\alpha \toᵤ \beta$.

UniformOnFun definition

(α β : Type*) (_ : Set (Set α))

Full source

/-- The type of functions from `α` to `β` equipped with the uniform structure and topology of
uniform convergence on some family `𝔖` of subsets of `α`. We denote it `α →ᵤ[𝔖] β`. -/
@[nolint unusedArguments]
def UniformOnFun (α β : Type*) (_ : Set (Set α)) :=
  α → β

Space of functions with uniform convergence on a family of sets

Informal description

Given types $\alpha$ and $\beta$, and a family $\mathfrak{S}$ of subsets of $\alpha$, the type $\alpha \to_{\mathfrak{S}} \beta$ represents the space of functions from $\alpha$ to $\beta$ equipped with the uniform structure and topology of uniform convergence on the family $\mathfrak{S}$.

UniformConvergence.term_→ᵤ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] scoped[UniformConvergence] notation:25 α " →ᵤ " β:0 => UniformFun α β

Uniform convergence function space notation

Informal description

The notation `α →ᵤ β` denotes the type of functions from `α` to `β` equipped with the uniform structure of uniform convergence. This is a type alias for `UniformFun α β`.

UniformConvergence.term_→ᵤ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] scoped[UniformConvergence] notation:25 α " →ᵤ[" 𝔖 "] " β:0 => UniformOnFun α β 𝔖

Uniform $\mathfrak{S}$-convergence function space notation

Informal description

The notation $ \alpha \toᵤ[\mathfrak{S}] \beta $ denotes the type of functions from $ \alpha $ to $ \beta $ equipped with the uniform structure of $\mathfrak{S}$-convergence, where $\mathfrak{S}$ is a specified family of subsets of $ \alpha $. This is a shorthand for `UniformOnFun α β 𝔖`.

instNonemptyUniformFun instance

[Nonempty β] : Nonempty (α →ᵤ β)

Full source

instance [Nonempty β] : Nonempty (α →ᵤ β) := Pi.instNonempty

Nonemptiness of Uniform Function Space

Informal description

If $\beta$ is a nonempty type, then the space of functions $\alpha \toᵤ \beta$ equipped with the uniform structure of uniform convergence is also nonempty.

instNonemptyUniformOnFun instance

[Nonempty β] : Nonempty (α →ᵤ[𝔖] β)

Full source

instance [Nonempty β] : Nonempty (α →ᵤ[𝔖] β) := Pi.instNonempty

Nonemptiness of Function Space with Uniform Convergence on a Family of Sets

Informal description

For any nonempty type $\beta$, the space of functions $\alpha \to_{\mathfrak{S}} \beta$ with uniform convergence on a family $\mathfrak{S}$ of subsets of $\alpha$ is nonempty.

instSubsingletonUniformFun instance

[Subsingleton β] : Subsingleton (α →ᵤ β)

Full source

instance [Subsingleton β] : Subsingleton (α →ᵤ β) :=
  inferInstanceAs <| Subsingleton <| α → β

Subsingleton Property of Uniform Function Space

Informal description

If $\beta$ is a subsingleton (i.e., has at most one element), then the space of functions $\alpha \toᵤ \beta$ equipped with the uniform structure of uniform convergence is also a subsingleton.

instSubsingletonUniformOnFun instance

[Subsingleton β] : Subsingleton (α →ᵤ[𝔖] β)

Full source

instance [Subsingleton β] : Subsingleton (α →ᵤ[𝔖] β) :=
  inferInstanceAs <| Subsingleton <| α → β

Subsingleton Property of Function Space with Uniform Convergence on a Family of Sets

Informal description

For any type $\beta$ that is a subsingleton (i.e., has at most one element), the space $\alpha \to_{\mathfrak{S}} \beta$ of functions from $\alpha$ to $\beta$ with uniform convergence on a family $\mathfrak{S}$ of subsets of $\alpha$ is also a subsingleton.

UniformFun.ofFun definition

: (α → β) ≃ (α →ᵤ β)

Full source

/-- Reinterpret `f : α → β` as an element of `α →ᵤ β`. -/
def UniformFun.ofFun : (α → β) ≃ (α →ᵤ β) :=
  ⟨fun x => x, fun x => x, fun _ => rfl, fun _ => rfl⟩

Reinterpretation of functions as uniform convergence functions

Informal description

The function `UniformFun.ofFun` is a bijection between the type of functions `α → β` and the type `α →ᵤ β` of functions equipped with the uniform structure of uniform convergence. It maps a function `f : α → β` to itself, reinterpreted as an element of `α →ᵤ β`, and its inverse similarly maps back to the original function space.

UniformOnFun.ofFun definition

(𝔖) : (α → β) ≃ (α →ᵤ[𝔖] β)

Full source

/-- Reinterpret `f : α → β` as an element of `α →ᵤ[𝔖] β`. -/
def UniformOnFun.ofFun (𝔖) : (α → β) ≃ (α →ᵤ[𝔖] β) :=
  ⟨fun x => x, fun x => x, fun _ => rfl, fun _ => rfl⟩

Reinterpretation of functions as uniform convergence functions on a family of sets

Informal description

The function `UniformOnFun.ofFun` is a bijection between the type of functions `α → β` and the type `α →ᵤ[𝔖] β` of functions equipped with the uniform structure of uniform convergence on a family `𝔖` of subsets of `α`. It maps a function `f : α → β` to itself, reinterpreted as an element of `α →ᵤ[𝔖] β`, and its inverse similarly maps back to the original function space.

UniformFun.toFun definition

: (α →ᵤ β) ≃ (α → β)

Full source

/-- Reinterpret `f : α →ᵤ β` as an element of `α → β`. -/
def UniformFun.toFun : (α →ᵤ β) ≃ (α → β) :=
  UniformFun.ofFun.symm

Conversion from uniform convergence functions to ordinary functions

Informal description

The function `UniformFun.toFun` is the inverse of `UniformFun.ofFun`, which maps an element of `α →ᵤ β$ (functions with the uniform structure of uniform convergence) back to the ordinary function space `α → β`.

UniformOnFun.toFun definition

(𝔖) : (α →ᵤ[𝔖] β) ≃ (α → β)

Full source

/-- Reinterpret `f : α →ᵤ[𝔖] β` as an element of `α → β`. -/
def UniformOnFun.toFun (𝔖) : (α →ᵤ[𝔖] β) ≃ (α → β) :=
  (UniformOnFun.ofFun 𝔖).symm

Conversion from uniform convergence functions to ordinary functions

Informal description

The function `UniformOnFun.toFun` is the inverse of `UniformOnFun.ofFun`, which maps an element of `α →ᵤ[𝔖] β` (functions with the uniform structure of uniform convergence on the family `𝔖` of subsets of `α`) back to the ordinary function space `α → β`.

UniformFun.toFun_ofFun theorem

(f : α → β) : toFun (ofFun f) = f

Full source

@[simp] lemma UniformFun.toFun_ofFun (f : α → β) : toFun (ofFun f) = f := rfl

Identity Property of Uniform Function Conversions: $\text{toFun} \circ \text{ofFun} = \text{id}$

Informal description

For any function $f \colon \alpha \to \beta$, the composition of the conversion maps `UniformFun.toFun` and `UniformFun.ofFun` applied to $f$ yields $f$ itself, i.e., $\text{toFun}(\text{ofFun}(f)) = f$.

UniformFun.ofFun_toFun theorem

(f : α →ᵤ β) : ofFun (toFun f) = f

Full source

@[simp] lemma UniformFun.ofFun_toFun (f : α →ᵤ β) : ofFun (toFun f) = f := rfl

Identity Property of Uniform Function Conversions: $\text{ofFun} \circ \text{toFun} = \text{id}$

Informal description

For any function $f$ in the uniform convergence function space $\alpha \toᵤ \beta$, the composition of the conversion to ordinary functions followed by the reinterpretation as uniform convergence functions returns $f$ itself, i.e., $\text{ofFun}(\text{toFun}(f)) = f$.

UniformOnFun.toFun_ofFun theorem

(f : α → β) : toFun 𝔖 (ofFun 𝔖 f) = f

Full source

@[simp] lemma UniformOnFun.toFun_ofFun (f : α → β) : toFun 𝔖 (ofFun 𝔖 f) = f := rfl

Identity of Function Conversion in Uniform $\mathfrak{S}$-Convergence Space

Informal description

For any function $f \colon \alpha \to \beta$, the composition of the conversion from $\alpha \to \beta$ to $\alpha \to_{\mathfrak{S}} \beta$ followed by the reverse conversion yields the original function $f$. That is, $\text{toFun}_{\mathfrak{S}} \circ \text{ofFun}_{\mathfrak{S}}(f) = f$.

UniformOnFun.ofFun_toFun theorem

(f : α →ᵤ[𝔖] β) : ofFun 𝔖 (toFun 𝔖 f) = f

Full source

@[simp] lemma UniformOnFun.ofFun_toFun (f : α →ᵤ[𝔖] β) : ofFun 𝔖 (toFun 𝔖 f) = f := rfl

Identity of Uniform Function Conversion: $\text{ofFun}_{\mathfrak{S}} \circ \text{toFun}_{\mathfrak{S}} = \text{id}$

Informal description

For any function $f$ in the space $\alpha \to_{\mathfrak{S}} \beta$ of functions with uniform convergence on the family $\mathfrak{S}$ of subsets of $\alpha$, the composition of the conversion to an ordinary function and back to the uniform convergence space yields the original function, i.e., $\text{ofFun}_{\mathfrak{S}}(\text{toFun}_{\mathfrak{S}}(f)) = f$.

UniformFun.gen definition

(V : Set (β × β)) : Set ((α →ᵤ β) × (α →ᵤ β))

Full source

/-- Basis sets for the uniformity of uniform convergence: `gen α β V` is the set of pairs `(f, g)`
of functions `α →ᵤ β` such that `∀ x, (f x, g x) ∈ V`. -/
protected def gen (V : Set (β × β)) : Set ((α →ᵤ β) × (α →ᵤ β)) :=
  { uv : (α →ᵤ β) × (α →ᵤ β) | ∀ x, (toFun uv.1 x, toFun uv.2 x) ∈ V }

Basis set for uniform convergence uniformity

Informal description

For a given set $V \subseteq \beta \times \beta$, the set $\text{gen}(\alpha, \beta, V)$ consists of all pairs of functions $(f, g) \in (\alpha \toᵤ \beta) \times (\alpha \toᵤ \beta)$ such that for every $x \in \alpha$, the pair $(f(x), g(x))$ belongs to $V$. This set forms a basis for the uniformity of uniform convergence on the function space $\alpha \toᵤ \beta$.

UniformFun.isBasis_gen theorem

(𝓑 : Filter <| β × β) : IsBasis (fun V : Set (β × β) => V ∈ 𝓑) (UniformFun.gen α β)

Full source

/-- If `𝓕` is a filter on `β × β`, then the set of all `UniformFun.gen α β V` for
`V ∈ 𝓕` is a filter basis on `(α →ᵤ β) × (α →ᵤ β)`. This will only be applied to `𝓕 = 𝓤 β` when
`β` is equipped with a `UniformSpace` structure, but it is useful to define it for any filter in
order to be able to state that it has a lower adjoint (see `UniformFun.gc`). -/
protected theorem isBasis_gen (𝓑 : Filter <| β × β) :
    IsBasis (fun V : Set (β × β) => V ∈ 𝓑) (UniformFun.gen α β) :=
  ⟨⟨univ, univ_mem⟩, @fun U V hU hV =>
    ⟨U ∩ V, inter_mem hU hV, fun _ huv => ⟨fun x => (huv x).left, fun x => (huv x).right⟩⟩⟩

Filter Basis Property of Uniform Convergence Generators

Informal description

Let $\mathfrak{B}$ be a filter on $\beta \times \beta$. Then the collection of sets $\text{gen}(\alpha, \beta, V)$ for all $V \in \mathfrak{B}$ forms a filter basis on $(\alpha \toᵤ \beta) \times (\alpha \toᵤ \beta)$. Here, $\text{gen}(\alpha, \beta, V)$ denotes the set of all pairs of functions $(f, g)$ such that $(f(x), g(x)) \in V$ for every $x \in \alpha$.

UniformFun.basis definition

(𝓕 : Filter <| β × β) : FilterBasis ((α →ᵤ β) × (α →ᵤ β))

Full source

/-- For `𝓕 : Filter (β × β)`, this is the set of all `UniformFun.gen α β V` for
`V ∈ 𝓕` as a bundled `FilterBasis` over `(α →ᵤ β) × (α →ᵤ β)`. This will only be applied to
`𝓕 = 𝓤 β` when `β` is equipped with a `UniformSpace` structure, but it is useful to define it for
any filter in order to be able to state that it has a lower adjoint
(see `UniformFun.gc`). -/
protected def basis (𝓕 : Filter <| β × β) : FilterBasis ((α →ᵤ β) × (α →ᵤ β)) :=
  (UniformFun.isBasis_gen α β 𝓕).filterBasis

Filter basis for uniform convergence uniformity

Informal description

For a given filter $\mathfrak{F}$ on $\beta \times \beta$, the filter basis $\text{basis}(\alpha, \beta, \mathfrak{F})$ consists of all sets $\text{gen}(\alpha, \beta, V)$ for $V \in \mathfrak{F}$, where $\text{gen}(\alpha, \beta, V)$ is the set of pairs $(f, g)$ of functions in $\alpha \toᵤ \beta$ such that $(f(x), g(x)) \in V$ for every $x \in \alpha$. This filter basis generates the uniformity of uniform convergence on the function space $\alpha \toᵤ \beta$.

UniformFun.filter definition

(𝓕 : Filter <| β × β) : Filter ((α →ᵤ β) × (α →ᵤ β))

Full source

/-- For `𝓕 : Filter (β × β)`, this is the filter generated by the filter basis
`UniformFun.basis α β 𝓕`. For `𝓕 = 𝓤 β`, this will be the uniformity of uniform
convergence on `α`. -/
protected def filter (𝓕 : Filter <| β × β) : Filter ((α →ᵤ β) × (α →ᵤ β)) :=
  (UniformFun.basis α β 𝓕).filter

Uniform convergence filter on function space

Informal description

Given a filter $\mathfrak{F}$ on $\beta \times \beta$, the filter $\text{filter}(\alpha, \beta, \mathfrak{F})$ is the filter on $(\alpha \toᵤ \beta) \times (\alpha \toᵤ \beta)$ generated by the filter basis $\text{basis}(\alpha, \beta, \mathfrak{F})$. When $\mathfrak{F}$ is the uniformity $\mathfrak{U}(\beta)$ on $\beta$, this filter becomes the uniformity of uniform convergence on the function space $\alpha \toᵤ \beta$.

UniformFun.phi definition

(α β : Type*) (uvx : ((α →ᵤ β) × (α →ᵤ β)) × α) : β × β

Full source

protected def phi (α β : Type*) (uvx : ((α →ᵤ β) × (α →ᵤ β)) × α) : β × β :=
  (uvx.fst.fst uvx.2, uvx.1.2 uvx.2)

Evaluation pairing for uniform convergence

Informal description

The function $\phi$ takes a pair of functions $(f, g)$ from $\alpha \toᵤ \beta$ and a point $x \in \alpha$, and returns the pair $(f(x), g(x))$ in $\beta \times \beta$. This is used to define the uniformity of uniform convergence on $\alpha \toᵤ \beta$.

UniformFun.gc theorem

: GaloisConnection lowerAdjoint fun 𝓕 => UniformFun.filter α β 𝓕

Full source

/-- The function `UniformFun.filter α β : Filter (β × β) → Filter ((α →ᵤ β) × (α →ᵤ β))`
has a lower adjoint `l` (in the sense of `GaloisConnection`). The exact definition of `l` is not
interesting; we will only use that it exists (in `UniformFun.mono` and
`UniformFun.iInf_eq`) and that
`l (Filter.map (Prod.map f f) 𝓕) = Filter.map (Prod.map ((∘) f) ((∘) f)) (l 𝓕)` for each
`𝓕 : Filter (γ × γ)` and `f : γ → α` (in `UniformFun.comap_eq`). -/
protected theorem gc : GaloisConnection lowerAdjoint fun 𝓕 => UniformFun.filter α β 𝓕 := by
  intro 𝓐 𝓕
  symm
  calc
    𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets := by
      rw [UniformFun.filter, ← FilterBasis.generate, le_generate_iff]
    _ ↔ ∀ U ∈ 𝓕, UniformFun.gen α β U ∈ 𝓐calc
    𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets := by
      rw [UniformFun.filter, ← FilterBasis.generate, le_generate_iff]
    _ ↔ ∀ U ∈ 𝓕, UniformFun.gen α β U ∈ 𝓐 := image_subset_iff
    _ ↔ ∀ U ∈ 𝓕,
          { uv | ∀ x, (uv, x) ∈ { t : ((α →ᵤ β) × (α →ᵤ β)) × α | (t.1.1 t.2, t.1.2 t.2) ∈ U } } ∈
            𝓐calc
    𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets := by
      rw [UniformFun.filter, ← FilterBasis.generate, le_generate_iff]
    _ ↔ ∀ U ∈ 𝓕, UniformFun.gen α β U ∈ 𝓐 := image_subset_iff
    _ ↔ ∀ U ∈ 𝓕,
          { uv | ∀ x, (uv, x) ∈ { t : ((α →ᵤ β) × (α →ᵤ β)) × α | (t.1.1 t.2, t.1.2 t.2) ∈ U } } ∈
            𝓐 :=
      Iff.rfl
    _ ↔ ∀ U ∈ 𝓕,
          { uvx : ((α →ᵤ β) × (α →ᵤ β)) × α | (uvx.1.1 uvx.2, uvx.1.2 uvx.2) ∈ U } ∈
            𝓐 ×ˢ (⊤ : Filter α)calc
    𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets := by
      rw [UniformFun.filter, ← FilterBasis.generate, le_generate_iff]
    _ ↔ ∀ U ∈ 𝓕, UniformFun.gen α β U ∈ 𝓐 := image_subset_iff
    _ ↔ ∀ U ∈ 𝓕,
          { uv | ∀ x, (uv, x) ∈ { t : ((α →ᵤ β) × (α →ᵤ β)) × α | (t.1.1 t.2, t.1.2 t.2) ∈ U } } ∈
            𝓐 :=
      Iff.rfl
    _ ↔ ∀ U ∈ 𝓕,
          { uvx : ((α →ᵤ β) × (α →ᵤ β)) × α | (uvx.1.1 uvx.2, uvx.1.2 uvx.2) ∈ U } ∈
            𝓐 ×ˢ (⊤ : Filter α) :=
      forall₂_congr fun U _hU => mem_prod_top.symm
    _ ↔ lowerAdjoint 𝓐 ≤ 𝓕 := Iff.rfl

Galois Connection for Uniform Convergence Filter

Informal description

The function $\text{UniformFun.filter}$ from filters on $\beta \times \beta$ to filters on $(\alpha \toᵤ \beta) \times (\alpha \toᵤ \beta)$ has a lower adjoint $l$ in the sense of a Galois connection. The exact definition of $l$ is not provided here, but we note its existence and the property that for any filter $\mathfrak{F}$ on $\gamma \times \gamma$ and any function $f : \gamma \to \alpha$, we have $l(\text{map}(f \times f, \mathfrak{F})) = \text{map}((f \circ -) \times (f \circ -), l(\mathfrak{F}))$.

UniformFun.uniformCore definition

: UniformSpace.Core (α →ᵤ β)

Full source

/-- Core of the uniform structure of uniform convergence. -/
protected def uniformCore : UniformSpace.Core (α →ᵤ β) :=
  UniformSpace.Core.mkOfBasis (UniformFun.basis α β (𝓤 β))
    (fun _ ⟨_, hV, hVU⟩ _ => hVU ▸ fun _ => refl_mem_uniformity hV)
    (fun _ ⟨V, hV, hVU⟩ =>
      hVU ▸
        ⟨UniformFun.gen α β (Prod.swap ⁻¹' V), ⟨Prod.swap ⁻¹' V, tendsto_swap_uniformity hV, rfl⟩,
          fun _ huv x => huv x⟩)
    fun _ ⟨_, hV, hVU⟩ =>
    hVU ▸
      let ⟨W, hW, hWV⟩ := comp_mem_uniformity_sets hV
      ⟨UniformFun.gen α β W, ⟨W, hW, rfl⟩, fun _ ⟨w, huw, hwv⟩ x => hWV ⟨w x, ⟨huw x, hwv x⟩⟩⟩

Core Uniform Structure of Uniform Convergence

Informal description

The core uniform structure of uniform convergence on the function space $\alpha \toᵤ \beta$ is generated by the basis sets $\text{gen}(\alpha, \beta, V)$ for $V$ in the uniformity of $\beta$, where $\text{gen}(\alpha, \beta, V)$ consists of all pairs $(f, g)$ of functions such that $(f(x), g(x)) \in V$ for every $x \in \alpha$. This core structure satisfies the uniformity axioms: reflexivity (every function is uniformly close to itself), symmetry (if $f$ is uniformly close to $g$, then $g$ is uniformly close to $f$), and transitivity (if $f$ is uniformly close to $g$ and $g$ is uniformly close to $h$, then $f$ is uniformly close to $h$).

UniformFun.uniformSpace instance

: UniformSpace (α →ᵤ β)

Full source

/-- Uniform structure of uniform convergence, declared as an instance on `α →ᵤ β`.
We will denote it `𝒰(α, β, uβ)` in the rest of this file. -/
instance uniformSpace : UniformSpace (α →ᵤ β) :=
  UniformSpace.ofCore (UniformFun.uniformCore α β)

Uniform Structure of Uniform Convergence on Function Space

Informal description

The function space $\alpha \toᵤ \beta$ of all functions from a type $\alpha$ to a uniform space $\beta$ is equipped with the uniform structure of uniform convergence. This uniform structure is generated by the sets $\{(f, g) \mid \forall x \in \alpha, (f(x), g(x)) \in V\}$ where $V$ ranges over the entourages of the uniform structure on $\beta$.

UniformFun.topologicalSpace instance

: TopologicalSpace (α →ᵤ β)

Full source

/-- Topology of uniform convergence, declared as an instance on `α →ᵤ β`. -/
instance topologicalSpace : TopologicalSpace (α →ᵤ β) :=
  inferInstance

Topology of Uniform Convergence on Function Spaces

Informal description

The function space $\alpha \toᵤ \beta$ of all functions from a type $\alpha$ to a uniform space $\beta$ is equipped with the topology of uniform convergence. This topology is induced by the uniform structure of uniform convergence, where a net of functions converges uniformly if and only if it converges uniformly at every point in $\alpha$.

UniformFun.hasBasis_uniformity theorem

: (𝓤 (α →ᵤ β)).HasBasis (· ∈ 𝓤 β) (UniformFun.gen α β)

Full source

/-- By definition, the uniformity of `α →ᵤ β` admits the family `{(f, g) | ∀ x, (f x, g x) ∈ V}`
for `V ∈ 𝓤 β` as a filter basis. -/
protected theorem hasBasis_uniformity :
    (𝓤 (α →ᵤ β)).HasBasis (· ∈ 𝓤 β) (UniformFun.gen α β) :=
  (UniformFun.isBasis_gen α β (𝓤 β)).hasBasis

Basis for Uniformity of Uniform Convergence on Function Space

Informal description

The uniformity $\mathcal{U}(\alpha \toᵤ \beta)$ on the function space $\alpha \toᵤ \beta$ has a basis consisting of sets of the form $\{(f, g) \mid \forall x \in \alpha, (f(x), g(x)) \in V\}$, where $V$ ranges over all entourages in the uniformity $\mathcal{U}(\beta)$ of $\beta$.

UniformFun.hasBasis_uniformity_of_basis theorem

 {ι : Sort*} {p : ι → Prop} {s : ι → Set (β × β)} (h : (𝓤 β).HasBasis p s) :
  (𝓤 (α →ᵤ β)).HasBasis p (UniformFun.gen α β ∘ s)

Full source

/-- The uniformity of `α →ᵤ β` admits the family `{(f, g) | ∀ x, (f x, g x) ∈ V}` for `V ∈ 𝓑` as
a filter basis, for any basis `𝓑` of `𝓤 β` (in the case `𝓑 = (𝓤 β).as_basis` this is true by
definition). -/
protected theorem hasBasis_uniformity_of_basis {ι : Sort*} {p : ι → Prop} {s : ι → Set (β × β)}
    (h : (𝓤 β).HasBasis p s) : (𝓤 (α →ᵤ β)).HasBasis p (UniformFun.genUniformFun.gen α β ∘ s) :=
  (UniformFun.hasBasis_uniformity α β).to_hasBasis
    (fun _ hU =>
      let ⟨i, hi, hiU⟩ := h.mem_iff.mp hU
      ⟨i, hi, fun _ huv x => hiU (huv x)⟩)
    fun i hi => ⟨s i, h.mem_of_mem hi, subset_refl _⟩

Basis for Uniformity of Uniform Convergence via Basis of Target Space

Informal description

Let $\beta$ be a uniform space with a basis $\mathfrak{B}$ for its uniformity $\mathcal{U}(\beta)$, indexed by a type $\iota$ with a predicate $p : \iota \to \text{Prop}$ and a family of sets $s : \iota \to \text{Set}(\beta \times \beta)$. If $\mathcal{U}(\beta)$ has basis $\mathfrak{B}$ (i.e., $h : \mathcal{U}(\beta).\text{HasBasis}\, p\, s$ holds), then the uniformity $\mathcal{U}(\alpha \toᵤ \beta)$ of uniform convergence on $\alpha \toᵤ \beta$ has a basis consisting of the sets $\text{gen}(\alpha, \beta, s(i))$ for $i \in \iota$ satisfying $p(i)$, where $\text{gen}(\alpha, \beta, V) := \{(f, g) \mid \forall x \in \alpha, (f(x), g(x)) \in V\}$.

UniformFun.hasBasis_nhds_of_basis theorem

 (f) {p : ι → Prop} {s : ι → Set (β × β)} (h : HasBasis (𝓤 β) p s) :
  (𝓝 f).HasBasis p fun i => {g | (f, g) ∈ UniformFun.gen α β (s i)}

Full source

/-- For `f : α →ᵤ β`, `𝓝 f` admits the family `{g | ∀ x, (f x, g x) ∈ V}` for `V ∈ 𝓑` as a filter
basis, for any basis `𝓑` of `𝓤 β`. -/
protected theorem hasBasis_nhds_of_basis (f) {p : ι → Prop} {s : ι → Set (β × β)}
    (h : HasBasis (𝓤 β) p s) :
    (𝓝 f).HasBasis p fun i => { g | (f, g) ∈ UniformFun.gen α β (s i) } :=
  nhds_basis_uniformity' (UniformFun.hasBasis_uniformity_of_basis α β h)

Basis for Neighborhood Filter in Uniform Convergence Space via Basis of Target Uniformity

Informal description

Let $\beta$ be a uniform space with a basis $\mathfrak{B}$ for its uniformity $\mathcal{U}(\beta)$, indexed by a type $\iota$ with a predicate $p : \iota \to \text{Prop}$ and a family of sets $s : \iota \to \text{Set}(\beta \times \beta)$. For any function $f \in \alpha \toᵤ \beta$, the neighborhood filter $\mathcal{N}(f)$ has a basis consisting of the sets $\{g \mid \forall x \in \alpha, (f(x), g(x)) \in s(i)\}$ for $i \in \iota$ satisfying $p(i)$.

UniformFun.hasBasis_nhds theorem

(f) : (𝓝 f).HasBasis (fun V => V ∈ 𝓤 β) fun V => {g | (f, g) ∈ UniformFun.gen α β V}

Full source

/-- For `f : α →ᵤ β`, `𝓝 f` admits the family `{g | ∀ x, (f x, g x) ∈ V}` for `V ∈ 𝓤 β` as a
filter basis. -/
protected theorem hasBasis_nhds (f) :
    (𝓝 f).HasBasis (fun V => V ∈ 𝓤 β) fun V => { g | (f, g) ∈ UniformFun.gen α β V } :=
  UniformFun.hasBasis_nhds_of_basis α β f (Filter.basis_sets _)

Basis for Neighborhood Filter in Uniform Convergence Space via Entourages of Target Space

Informal description

For any function $f \in \alpha \toᵤ \beta$, the neighborhood filter $\mathcal{N}(f)$ has a basis consisting of sets of the form $\{g \mid \forall x \in \alpha, (f(x), g(x)) \in V\}$ where $V$ ranges over all entourages in the uniformity $\mathcal{U}(\beta)$ of $\beta$.

UniformFun.uniformContinuous_eval theorem

(x : α) : UniformContinuous (Function.eval x ∘ toFun : (α →ᵤ β) → β)

Full source

/-- Evaluation at a fixed point is uniformly continuous on `α →ᵤ β`. -/
theorem uniformContinuous_eval (x : α) :
    UniformContinuous (Function.evalFunction.eval x ∘ toFun : (α →ᵤ β) → β) := by
  change _ ≤ _
  rw [map_le_iff_le_comap,
    (UniformFun.hasBasis_uniformity α β).le_basis_iff ((𝓤 _).basis_sets.comap _)]
  exact fun U hU => ⟨U, hU, fun uv huv => huv x⟩

Uniform Continuity of Point Evaluation in Uniform Convergence Space

Informal description

For any fixed point $x \in \alpha$, the evaluation map $\text{eval}_x : \alpha \toᵤ \beta \to \beta$, defined by $\text{eval}_x(f) = f(x)$, is uniformly continuous with respect to the uniform structure of uniform convergence on $\alpha \toᵤ \beta$ and the given uniform structure on $\beta$.

UniformFun.mem_gen theorem

 {β} {f g : α →ᵤ β} {V : Set (β × β)} : (f, g) ∈ UniformFun.gen α β V ↔ ∀ x, (toFun f x, toFun g x) ∈ V

Full source

@[simp]
protected lemma mem_gen {β} {f g : α →ᵤ β} {V : Set (β × β)} :
    (f, g)(f, g) ∈ UniformFun.gen α β V(f, g) ∈ UniformFun.gen α β V ↔ ∀ x, (toFun f x, toFun g x) ∈ V :=
  .rfl

Characterization of Uniform Convergence Basis Set Membership

Informal description

For any functions $f, g \in \alpha \toᵤ \beta$ and any set $V \subseteq \beta \times \beta$, the pair $(f, g)$ belongs to the uniform convergence basis set $\text{gen}(\alpha, \beta, V)$ if and only if for every $x \in \alpha$, the pair of evaluations $(f(x), g(x))$ belongs to $V$.

UniformFun.mono theorem

: Monotone (@UniformFun.uniformSpace α γ)

Full source

/-- If `u₁` and `u₂` are two uniform structures on `γ` and `u₁ ≤ u₂`, then
`𝒰(α, γ, u₁) ≤ 𝒰(α, γ, u₂)`. -/
protected theorem mono : Monotone (@UniformFun.uniformSpace α γ) := fun _ _ hu =>
  (UniformFun.gc α γ).monotone_u hu

Monotonicity of Uniform Convergence Structure with Respect to Target Uniformity

Informal description

For any type $\alpha$ and uniform space $\gamma$, the uniform structure $\mathcal{U}(\alpha, \gamma, u)$ on the function space $\alpha \toᵤ \gamma$ is monotone with respect to the uniform structure $u$ on $\gamma$. That is, if $u_1$ and $u_2$ are uniform structures on $\gamma$ with $u_1 \leq u_2$, then $\mathcal{U}(\alpha, \gamma, u_1) \leq \mathcal{U}(\alpha, \gamma, u_2)$.

UniformFun.iInf_eq theorem

{u : ι → UniformSpace γ} : 𝒰(α, γ, (⨅ i, u i)) = ⨅ i, 𝒰(α, γ, u i)

Full source

/-- If `u` is a family of uniform structures on `γ`, then
`𝒰(α, γ, (⨅ i, u i)) = ⨅ i, 𝒰(α, γ, u i)`. -/
protected theorem iInf_eq {u : ι → UniformSpace γ} : 𝒰(α, γ, (⨅ i, u i)) = ⨅ i, 𝒰(α, γ, u i) := by
  -- This follows directly from the fact that the upper adjoint in a Galois connection maps
  -- infimas to infimas.
  ext : 1
  change UniformFun.filter α γ 𝓤[⨅ i, u i] = 𝓤[⨅ i, 𝒰(α, γ, u i)]
  rw [iInf_uniformity, iInf_uniformity]
  exact (UniformFun.gc α γ).u_iInf

Infimum Commutes with Uniform Convergence Structure: $\mathcal{U}(\alpha, \gamma, \bigsqcap_i u_i) = \bigsqcap_i \mathcal{U}(\alpha, \gamma, u_i)$

Informal description

For any family of uniform structures $\{u_i\}_{i \in \iota}$ on a type $\gamma$, the uniform structure of uniform convergence on $\alpha \toᵤ \gamma$ with respect to the infimum uniform structure $\bigsqcap_i u_i$ is equal to the infimum of the uniform structures of uniform convergence on $\alpha \toᵤ \gamma$ with respect to each $u_i$. That is, \[ \mathcal{U}(\alpha, \gamma, \bigsqcap_i u_i) = \bigsqcap_i \mathcal{U}(\alpha, \gamma, u_i). \]

UniformFun.inf_eq theorem

{u₁ u₂ : UniformSpace γ} : 𝒰(α, γ, u₁ ⊓ u₂) = 𝒰(α, γ, u₁) ⊓ 𝒰(α, γ, u₂)

Full source

/-- If `u₁` and `u₂` are two uniform structures on `γ`, then
`𝒰(α, γ, u₁ ⊓ u₂) = 𝒰(α, γ, u₁) ⊓ 𝒰(α, γ, u₂)`. -/
protected theorem inf_eq {u₁ u₂ : UniformSpace γ} :
    𝒰(α, γ, u₁ ⊓ u₂) = 𝒰(α, γ, u₁)𝒰(α, γ, u₁) ⊓ 𝒰(α, γ, u₂) := by
  -- This follows directly from the fact that the upper adjoint in a Galois connection maps
  -- infimas to infimas.
  rw [inf_eq_iInf, inf_eq_iInf, UniformFun.iInf_eq]
  refine iInf_congr fun i => ?_
  cases i <;> rfl

Infimum of Uniform Structures Commutes with Uniform Convergence: $\mathcal{U}(\alpha, \gamma, u₁ ⊓ u₂) = \mathcal{U}(\alpha, \gamma, u₁) ⊓ \mathcal{U}(\alpha, \gamma, u₂)$

Informal description

For any two uniform structures $u₁$ and $u₂$ on a type $\gamma$, the uniform structure of uniform convergence on the function space $\alpha \toᵤ \gamma$ with respect to the infimum $u₁ ⊓ u₂$ is equal to the infimum of the uniform structures of uniform convergence with respect to $u₁$ and $u₂$ individually. That is, \[ \mathcal{U}(\alpha, \gamma, u₁ ⊓ u₂) = \mathcal{U}(\alpha, \gamma, u₁) ⊓ \mathcal{U}(\alpha, \gamma, u₂). \]

UniformFun.postcomp_isUniformInducing theorem

 [UniformSpace γ] {f : γ → β} (hf : IsUniformInducing f) :
  IsUniformInducing (ofFun ∘ (f ∘ ·) ∘ toFun : (α →ᵤ γ) → α →ᵤ β)

Full source

/-- Post-composition by a uniform inducing function is
a uniform inducing function for the uniform structures of uniform convergence.

More precisely, if `f : γ → β` is uniform inducing,
then `(f ∘ ·) : (α →ᵤ γ) → (α →ᵤ β)` is uniform inducing. -/
lemma postcomp_isUniformInducing [UniformSpace γ] {f : γ → β}
    (hf : IsUniformInducing f) : IsUniformInducing (ofFunofFun ∘ (f ∘ ·) ∘ toFun : (α →ᵤ γ) → α →ᵤ β) :=
  ⟨((UniformFun.hasBasis_uniformity _ _).comap _).eq_of_same_basis <|
    UniformFun.hasBasis_uniformity_of_basis _ _ (hf.basis_uniformity (𝓤 β).basis_sets)⟩

Post-composition by a Uniform Inducing Map is Uniform Inducing for Uniform Convergence

Informal description

Let $\gamma$ and $\beta$ be uniform spaces, and let $f : \gamma \to \beta$ be a uniform inducing map. Then the post-composition map $(f \circ \cdot) : (\alpha \toᵤ \gamma) \to (\alpha \toᵤ \beta)$ is also uniform inducing, where $\alpha \toᵤ \gamma$ and $\alpha \toᵤ \beta$ denote the function spaces equipped with the uniform structures of uniform convergence.

UniformFun.postcomp_isUniformEmbedding theorem

 [UniformSpace γ] {f : γ → β} (hf : IsUniformEmbedding f) :
  IsUniformEmbedding (ofFun ∘ (f ∘ ·) ∘ toFun : (α →ᵤ γ) → α →ᵤ β)

Full source

/-- Post-composition by a uniform embedding is
a uniform embedding for the uniform structures of uniform convergence.

More precisely, if `f : γ → β` is a uniform embedding,
then `(f ∘ ·) : (α →ᵤ γ) → (α →ᵤ β)` is a uniform embedding. -/
protected theorem postcomp_isUniformEmbedding [UniformSpace γ] {f : γ → β}
    (hf : IsUniformEmbedding f) :
    IsUniformEmbedding (ofFunofFun ∘ (f ∘ ·) ∘ toFun : (α →ᵤ γ) → α →ᵤ β) where
  toIsUniformInducing := UniformFun.postcomp_isUniformInducing hf.isUniformInducing
  injective _ _ H := funext fun _ ↦ hf.injective (congrFun H _)

Post-composition by a Uniform Embedding is a Uniform Embedding for Uniform Convergence

Informal description

Let $\gamma$ and $\beta$ be uniform spaces, and let $f : \gamma \to \beta$ be a uniform embedding. Then the post-composition map $(f \circ \cdot) : (\alpha \toᵤ \gamma) \to (\alpha \toᵤ \beta)$ is also a uniform embedding, where $\alpha \toᵤ \gamma$ and $\alpha \toᵤ \beta$ denote the function spaces equipped with the uniform structures of uniform convergence.

UniformFun.comap_eq theorem

{f : γ → β} : 𝒰(α, γ, ‹UniformSpace β›.comap f) = 𝒰(α, β, _).comap (f ∘ ·)

Full source

/-- If `u` is a uniform structures on `β` and `f : γ → β`, then
`𝒰(α, γ, comap f u) = comap (fun g ↦ f ∘ g) 𝒰(α, γ, u₁)`. -/
protected theorem comap_eq {f : γ → β} :
    𝒰(α, γ, ‹UniformSpace β›.comap f) = 𝒰(α, β, _).comap (f ∘ ·) := by
  letI : UniformSpace γ := .comap f ‹_›
  exact (UniformFun.postcomp_isUniformInducing (f := f) ⟨rfl⟩).comap_uniformSpace.symm

Uniform structure of uniform convergence commutes with pullback via composition: $\mathcal{U}(\alpha, \gamma, f^*\mathcal{U}_\beta) = (f \circ \cdot)^* \mathcal{U}(\alpha, \beta, \mathcal{U}_\beta)$

Informal description

Let $\beta$ be a uniform space and $f : \gamma \to \beta$ be a function. Then the uniform structure of uniform convergence on $\alpha \to \gamma$ induced by the pullback uniform structure on $\gamma$ (via $f$) is equal to the pullback of the uniform structure of uniform convergence on $\alpha \to \beta$ under the post-composition map $g \mapsto f \circ g$.

UniformFun.postcomp_uniformContinuous theorem

 [UniformSpace γ] {f : γ → β} (hf : UniformContinuous f) :
  UniformContinuous (ofFun ∘ (f ∘ ·) ∘ toFun : (α →ᵤ γ) → α →ᵤ β)

Full source

/-- Post-composition by a uniformly continuous function is uniformly continuous on `α →ᵤ β`.

More precisely, if `f : γ → β` is uniformly continuous, then `(fun g ↦ f ∘ g) : (α →ᵤ γ) → (α →ᵤ β)`
is uniformly continuous. -/
protected theorem postcomp_uniformContinuous [UniformSpace γ] {f : γ → β}
    (hf : UniformContinuous f) :
    UniformContinuous (ofFunofFun ∘ (f ∘ ·) ∘ toFun : (α →ᵤ γ) → α →ᵤ β) := by
  -- This is a direct consequence of `UniformFun.comap_eq`
    refine uniformContinuous_iff.mpr ?_
    exact (UniformFun.mono (uniformContinuous_iff.mp hf)).trans_eq UniformFun.comap_eq

Uniform Continuity of Post-Composition in Uniform Convergence Spaces

Informal description

Let $\gamma$ and $\beta$ be uniform spaces, and let $f : \gamma \to \beta$ be a uniformly continuous function. Then the post-composition map $(f \circ \cdot) : (\alpha \toᵤ \gamma) \to (\alpha \toᵤ \beta)$ is uniformly continuous, where $\alpha \toᵤ \gamma$ and $\alpha \toᵤ \beta$ denote the function spaces equipped with the uniform structures of uniform convergence.

UniformFun.congrRight definition

[UniformSpace γ] (e : γ ≃ᵤ β) : (α →ᵤ γ) ≃ᵤ (α →ᵤ β)

Full source

/-- Turn a uniform isomorphism `γ ≃ᵤ β` into a uniform isomorphism `(α →ᵤ γ) ≃ᵤ (α →ᵤ β)` by
post-composing. -/
protected def congrRight [UniformSpace γ] (e : γ ≃ᵤ β) : (α →ᵤ γ) ≃ᵤ (α →ᵤ β) :=
  { Equiv.piCongrRight fun _ => e.toEquiv with
    uniformContinuous_toFun := UniformFun.postcomp_uniformContinuous e.uniformContinuous
    uniformContinuous_invFun := UniformFun.postcomp_uniformContinuous e.symm.uniformContinuous }

Uniform isomorphism of function spaces via post-composition

Informal description

Given a uniform isomorphism $ e : \gamma \simeq \beta $ between uniform spaces, the post-composition map $ (f \mapsto e \circ f) $ induces a uniform isomorphism between the function spaces $ \alpha \toᵤ \gamma $ and $ \alpha \toᵤ \beta $ equipped with their respective uniform convergence structures.

UniformFun.precomp_uniformContinuous theorem

{f : γ → α} : UniformContinuous fun g : α →ᵤ β => ofFun (toFun g ∘ f)

Full source

/-- Pre-composition by any function is uniformly continuous for the uniform structures of
uniform convergence.

More precisely, for any `f : γ → α`, the function `(· ∘ f) : (α →ᵤ β) → (γ →ᵤ β)` is uniformly
continuous. -/
protected theorem precomp_uniformContinuous {f : γ → α} :
    UniformContinuous fun g : α →ᵤ β => ofFun (toFuntoFun g ∘ f) := by
  -- Here we simply go back to filter bases.
  rw [UniformContinuous,
      (UniformFun.hasBasis_uniformity α β).tendsto_iff (UniformFun.hasBasis_uniformity γ β)]
  exact fun U hU => ⟨U, hU, fun uv huv x => huv (f x)⟩

Uniform continuity of pre-composition in uniform convergence spaces

Informal description

For any function $f \colon \gamma \to \alpha$, the pre-composition map $g \mapsto g \circ f$ is uniformly continuous from the function space $\alpha \toᵤ \beta$ (equipped with the uniform structure of uniform convergence) to $\gamma \toᵤ \beta$.

UniformFun.congrLeft definition

(e : γ ≃ α) : (γ →ᵤ β) ≃ᵤ (α →ᵤ β)

Full source

/-- Turn a bijection `γ ≃ α` into a uniform isomorphism
`(γ →ᵤ β) ≃ᵤ (α →ᵤ β)` by pre-composing. -/
protected def congrLeft (e : γ ≃ α) : (γ →ᵤ β) ≃ᵤ (α →ᵤ β) where
  toEquiv := e.arrowCongr (.refl _)
  uniformContinuous_toFun := UniformFun.precomp_uniformContinuous
  uniformContinuous_invFun := UniformFun.precomp_uniformContinuous

Uniform isomorphism of function spaces induced by domain bijection

Informal description

Given a bijection $e : \gamma \simeq \alpha$ between types $\gamma$ and $\alpha$, the function `UniformFun.congrLeft` constructs a uniform isomorphism between the function spaces $\gamma \toᵤ \beta$ and $\alpha \toᵤ \beta$ by pre-composition with $e$. Specifically: - The forward map sends $f : \gamma \to \beta$ to $f \circ e^{-1} : \alpha \to \beta$ - The inverse map sends $g : \alpha \to \beta$ to $g \circ e : \gamma \to \beta$ Both maps are uniformly continuous, establishing a uniform isomorphism between the two function spaces equipped with their respective uniform structures of uniform convergence.

UniformFun.uniformContinuous_toFun theorem

: UniformContinuous (toFun : (α →ᵤ β) → α → β)

Full source

/-- The natural map `UniformFun.toFun` from `α →ᵤ β` to `α → β` is uniformly continuous.

In other words, the uniform structure of uniform convergence is finer than that of pointwise
convergence, aka the product uniform structure. -/
protected theorem uniformContinuous_toFun : UniformContinuous (toFun : (α →ᵤ β) → α → β) := by
  -- By definition of the product uniform structure, this is just `uniform_continuous_eval`.
  rw [uniformContinuous_pi]
  intro x
  exact uniformContinuous_eval β x

Uniform continuity of the natural map from uniform convergence to pointwise convergence

Informal description

The natural map from the space of uniformly convergent functions $\alpha \toᵤ \beta$ to the space of all functions $\alpha \to \beta$ is uniformly continuous. In other words, the uniform structure of uniform convergence is finer than the uniform structure of pointwise convergence (the product uniform structure).

UniformFun.instT2Space instance

[T2Space β] : T2Space (α →ᵤ β)

Full source

/-- The topology of uniform convergence is T₂. -/
instance [T2Space β] : T2Space (α →ᵤ β) :=
  .of_injective_continuous toFun.injective UniformFun.uniformContinuous_toFun.continuous

Hausdorff Property of Uniform Convergence Function Space

Informal description

For any uniform space $\beta$ that is a Hausdorff space, the function space $\alpha \toᵤ \beta$ equipped with the uniform structure of uniform convergence is also a Hausdorff space.

UniformFun.tendsto_iff_tendstoUniformly theorem

{F : ι → α →ᵤ β} {f : α →ᵤ β} : Tendsto F p (𝓝 f) ↔ TendstoUniformly (toFun ∘ F) (toFun f) p

Full source

/-- The topology of uniform convergence indeed gives the same notion of convergence as
`TendstoUniformly`. -/
protected theorem tendsto_iff_tendstoUniformly {F : ι → α →ᵤ β} {f : α →ᵤ β} :
    TendstoTendsto F p (𝓝 f) ↔ TendstoUniformly (toFun ∘ F) (toFun f) p := by
  rw [(UniformFun.hasBasis_nhds α β f).tendsto_right_iff, TendstoUniformly]
  simp only [mem_setOf, UniformFun.gen, Function.comp_def]

Equivalence of Uniform Convergence and Pointwise Uniform Convergence in Function Space

Informal description

Let $\alpha$ be a type, $\beta$ be a uniform space, and $F : \iota \to \alpha \toᵤ \beta$ be a net of functions. For a function $f \in \alpha \toᵤ \beta$, the net $F$ converges to $f$ in the topology of uniform convergence if and only if the net of functions $\text{toFun} \circ F$ converges uniformly to $\text{toFun}(f)$.

UniformFun.uniformEquivProdArrow definition

[UniformSpace γ] : (α →ᵤ β × γ) ≃ᵤ (α →ᵤ β) × (α →ᵤ γ)

Full source

/-- The natural bijection between `α → β × γ` and `(α → β) × (α → γ)`, upgraded to a uniform
isomorphism between `α →ᵤ β × γ` and `(α →ᵤ β) × (α →ᵤ γ)`. -/
protected def uniformEquivProdArrow [UniformSpace γ] : (α →ᵤ β × γ) ≃ᵤ (α →ᵤ β) × (α →ᵤ γ) :=
  -- Denote `φ` this bijection. We want to show that
  -- `comap φ (𝒰(α, β, uβ) × 𝒰(α, γ, uγ)) = 𝒰(α, β × γ, uβ × uγ)`.
  -- But `uβ × uγ` is defined as `comap fst uβ ⊓ comap snd uγ`, so we just have to apply
  -- `UniformFun.inf_eq` and `UniformFun.comap_eq`, which leaves us to check
  -- that some square commutes.
  Equiv.toUniformEquivOfIsUniformInducing (Equiv.arrowProdEquivProdArrow _ _ _) <| by
    constructor
    change
      comap (Prod.map (Equiv.arrowProdEquivProdArrow _ _ _) (Equiv.arrowProdEquivProdArrow _ _ _))
          _ = _
    simp_rw [UniformFun]
    rw [← uniformity_comap]
    congr
    unfold instUniformSpaceProd
    rw [UniformSpace.comap_inf, ← UniformSpace.comap_comap, ← UniformSpace.comap_comap]
    have := (@UniformFun.inf_eq α (β × γ)
      (UniformSpace.comap Prod.fst ‹_›) (UniformSpace.comap Prod.snd ‹_›)).symm
    rwa [UniformFun.comap_eq, UniformFun.comap_eq] at this

Uniform isomorphism between product-valued functions and pairs of functions under uniform convergence

Informal description

The natural bijection between the function space $\alpha \to \beta \times \gamma$ and the product space $(\alpha \to \beta) \times (\alpha \to \gamma)$, upgraded to a uniform isomorphism between the uniform convergence spaces $\alpha \toᵤ (\beta \times \gamma)$ and $(\alpha \toᵤ \beta) \times (\alpha \toᵤ \gamma)$. This isomorphism preserves the uniform structures, meaning that uniform convergence in $\alpha \toᵤ (\beta \times \gamma)$ corresponds to uniform convergence in both components of $(\alpha \toᵤ \beta) \times (\alpha \toᵤ \gamma)$.

UniformFun.uniformEquivPiComm definition

: UniformEquiv (α →ᵤ ∀ i, δ i) (∀ i, α →ᵤ δ i)

Full source

/-- The natural bijection between `α → Π i, δ i` and `Π i, α → δ i`, upgraded to a uniform
isomorphism between `α →ᵤ (Π i, δ i)` and `Π i, α →ᵤ δ i`. -/
protected def uniformEquivPiComm : UniformEquiv (α →ᵤ ∀ i, δ i) (∀ i, α →ᵤ δ i) :=
  -- Denote `φ` this bijection. We want to show that
    -- `comap φ (Π i, 𝒰(α, δ i, uδ i)) = 𝒰(α, (Π i, δ i), (Π i, uδ i))`.
    -- But `Π i, uδ i` is defined as `⨅ i, comap (eval i) (uδ i)`, so we just have to apply
    -- `UniformFun.iInf_eq` and `UniformFun.comap_eq`, which leaves us to check
    -- that some square commutes.
    @Equiv.toUniformEquivOfIsUniformInducing
    _ _ 𝒰(α, ∀ i, δ i, Pi.uniformSpace δ)
    (@Pi.uniformSpace ι (fun i => α → δ i) fun i => 𝒰(α, δ i, _)) (Equiv.piComm _) <| by
      refine @IsUniformInducing.mk ?_ ?_ ?_ ?_ ?_ ?_
      change comap (Prod.map Function.swap Function.swap) _ = _
      rw [← uniformity_comap]
      congr
      unfold Pi.uniformSpace
      rw [UniformSpace.ofCoreEq_toCore, UniformSpace.ofCoreEq_toCore,
        UniformSpace.comap_iInf, UniformFun.iInf_eq]
      refine iInf_congr fun i => ?_
      rw [← UniformSpace.comap_comap, UniformFun.comap_eq]
      rfl

Uniform isomorphism between function space and product space under uniform convergence

Informal description

The natural bijection between the function space $\alpha \to \prod_i \delta_i$ (equipped with the uniform structure of uniform convergence) and the product space $\prod_i (\alpha \to \delta_i)$ (where each component $\alpha \to \delta_i$ is equipped with the uniform structure of uniform convergence) is a uniform isomorphism. This means that the uniform structure on $\alpha \to \prod_i \delta_i$ coincides with the product uniform structure obtained by uniformly converging in each component separately.

UniformFun.isClosed_setOf_continuous theorem

[TopologicalSpace α] : IsClosed {f : α →ᵤ β | Continuous (toFun f)}

Full source

/-- The set of continuous functions is closed in the uniform convergence topology.
This is a simple wrapper over `TendstoUniformly.continuous`. -/
theorem isClosed_setOf_continuous [TopologicalSpace α] :
    IsClosed {f : α →ᵤ β | Continuous (toFun f)} := by
  refine isClosed_iff_forall_filter.2 fun f u _ hu huf ↦ ?_
  rw [← tendsto_id', UniformFun.tendsto_iff_tendstoUniformly] at huf
  exact huf.continuous (le_principal_iff.mp hu)

Closedness of Continuous Functions in Uniform Convergence Topology

Informal description

Let $\alpha$ be a topological space and $\beta$ be a uniform space. The set of continuous functions from $\alpha$ to $\beta$ is closed in the space $\alpha \toᵤ \beta$ equipped with the topology of uniform convergence.

UniformFun.uniformSpace_eq_inf_precomp_of_cover theorem

 {δ₁ δ₂ : Type*} (φ₁ : δ₁ → α) (φ₂ : δ₂ → α) (h_cover : range φ₁ ∪ range φ₂ = univ) :
  𝒰(α, β, _) = .comap (ofFun ∘ (· ∘ φ₁) ∘ toFun) 𝒰(δ₁, β, _) ⊓ .comap (ofFun ∘ (· ∘ φ₂) ∘ toFun) 𝒰(δ₂, β, _)

Full source

theorem uniformSpace_eq_inf_precomp_of_cover {δ₁ δ₂ : Type*} (φ₁ : δ₁ → α) (φ₂ : δ₂ → α)
    (h_cover : rangerange φ₁ ∪ range φ₂ = univ) :
    𝒰(α, β, _) =
      .comap.comap (ofFun ∘ (· ∘ φ₁) ∘ toFun) 𝒰(δ₁, β, _) ⊓
      .comap (ofFun ∘ (· ∘ φ₂) ∘ toFun) 𝒰(δ₂, β, _) := by
  ext : 1
  refine le_antisymm (le_inf ?_ ?_) ?_
  · exact tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous
  · exact tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous
  · refine
      (UniformFun.hasBasis_uniformity δ₁ β |>.comap _).inf
      (UniformFun.hasBasis_uniformity δ₂ β |>.comap _)
        |>.le_basis_iff (UniformFun.hasBasis_uniformity α β) |>.mpr fun U hU ↦
        ⟨⟨U, U⟩, ⟨hU, hU⟩, fun ⟨f, g⟩ hfg x ↦ ?_⟩
    rcases h_cover.ge <| mem_univ x with (⟨y, rfl⟩|⟨y, rfl⟩)
    · exact hfg.1 y
    · exact hfg.2 y

Uniform Structure of Uniform Convergence as Infimum of Precomposition Pullbacks

Informal description

Let $\alpha$ and $\beta$ be types, with $\beta$ equipped with a uniform structure. For any functions $\phi_1 \colon \delta_1 \to \alpha$ and $\phi_2 \colon \delta_2 \to \alpha$ such that the union of their ranges covers $\alpha$, the uniform structure of uniform convergence on $\alpha \to \beta$ is equal to the infimum of the pullbacks of the uniform structures of uniform convergence on $\delta_1 \to \beta$ and $\delta_2 \to \beta$ under the precomposition maps $g \mapsto g \circ \phi_1$ and $g \mapsto g \circ \phi_2$, respectively.

UniformFun.uniformSpace_eq_iInf_precomp_of_cover theorem

 {δ : ι → Type*} (φ : Π i, δ i → α) (h_cover : ∃ I : Set ι, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ) :
  𝒰(α, β, _) = ⨅ i, .comap (ofFun ∘ (· ∘ φ i) ∘ toFun) 𝒰(δ i, β, _)

Full source

theorem uniformSpace_eq_iInf_precomp_of_cover {δ : ι → Type*} (φ : Π i, δ i → α)
    (h_cover : ∃ I : Set ι, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ) :
    𝒰(α, β, _) = ⨅ i, .comap (ofFun ∘ (· ∘ φ i) ∘ toFun) 𝒰(δ i, β, _) := by
  ext : 1
  simp_rw [iInf_uniformity, uniformity_comap]
  refine le_antisymm (le_iInf fun i ↦ tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous) ?_
  rcases h_cover with ⟨I, I_finite, I_cover⟩
  refine Filter.hasBasis_iInf (fun i : ι ↦ UniformFun.hasBasis_uniformity (δ i) β |>.comap _)
      |>.le_basis_iff (UniformFun.hasBasis_uniformity α β) |>.mpr fun U hU ↦
    ⟨⟨I, fun _ ↦ U⟩, ⟨I_finite, fun _ ↦ hU⟩, fun ⟨f, g⟩ hfg x ↦ ?_⟩
  rcases mem_iUnion₂.mp <| I_cover.ge <| mem_univ x with ⟨i, hi, y, rfl⟩
  exact mem_iInter.mp hfg ⟨i, hi⟩ y

Uniform Structure of Uniform Convergence as Infimum of Precomposition Structures under Finite Cover Condition

Informal description

Let $\{\delta_i\}_{i \in \iota}$ be a family of types, and let $\varphi_i : \delta_i \to \alpha$ be a family of functions indexed by $\iota$. Suppose there exists a finite subset $I \subseteq \iota$ such that the union of the ranges of $\varphi_i$ for $i \in I$ covers $\alpha$ (i.e., $\bigcup_{i \in I} \text{range}(\varphi_i) = \alpha$). Then the uniform structure of uniform convergence on $\alpha \to \beta$ is equal to the infimum of the uniform structures obtained by precomposing with each $\varphi_i$ and pulling back the uniform structure of uniform convergence on $\delta_i \to \beta$.

UniformOnFun.gen definition

(𝔖) (S : Set α) (V : Set (β × β)) : Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))

Full source

/-- Basis sets for the uniformity of `𝔖`-convergence: for `S : Set α` and `V : Set (β × β)`,
`gen 𝔖 S V` is the set of pairs `(f, g)` of functions `α →ᵤ[𝔖] β` such that
`∀ x ∈ S, (f x, g x) ∈ V`. Note that the family `𝔖 : Set (Set α)` is only used to specify which
type alias of `α → β` to use here. -/
protected def gen (𝔖) (S : Set α) (V : Set (β × β)) : Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) :=
  { uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) | ∀ x ∈ S, (toFun 𝔖 uv.1 x, toFun 𝔖 uv.2 x) ∈ V }

Basis set for $\mathfrak{S}$-convergence uniformity

Informal description

For a family of subsets $\mathfrak{S}$ of $\alpha$ and a set $V \subseteq \beta \times \beta$, the set $\text{gen}_{\mathfrak{S}}(S, V)$ consists of all pairs of functions $(f, g)$ in $\alpha \to_{\mathfrak{S}} \beta$ such that for every $x \in S$, the pair $(f(x), g(x))$ belongs to $V$.

UniformOnFun.gen_eq_preimage_restrict theorem

 {𝔖} (S : Set α) (V : Set (β × β)) :
  UniformOnFun.gen 𝔖 S V =
    Prod.map (S.restrict ∘ UniformFun.toFun) (S.restrict ∘ UniformFun.toFun) ⁻¹' UniformFun.gen S β V

Full source

/-- For `S : Set α` and `V : Set (β × β)`, we have
`UniformOnFun.gen 𝔖 S V = (S.restrict × S.restrict) ⁻¹' (UniformFun.gen S β V)`.
This is the crucial fact for proving that the family `UniformOnFun.gen S V` for `S ∈ 𝔖` and
`V ∈ 𝓤 β` is indeed a basis for the uniformity `α →ᵤ[𝔖] β` endowed with `𝒱(α, β, 𝔖, uβ)`
the uniform structure of `𝔖`-convergence, as defined in `UniformOnFun.uniformSpace`. -/
protected theorem gen_eq_preimage_restrict {𝔖} (S : Set α) (V : Set (β × β)) :
    UniformOnFun.gen 𝔖 S V =
      Prod.mapProd.map (S.restrict ∘ UniformFun.toFun) (S.restrict ∘ UniformFun.toFun) ⁻¹'
        UniformFun.gen S β V := by
  ext uv
  exact ⟨fun h ⟨x, hx⟩ => h x hx, fun h x hx => h ⟨x, hx⟩⟩

Basis Set for $\mathfrak{S}$-Convergence as Preimage of Uniform Convergence Basis

Informal description

For a subset $S \subseteq \alpha$ and a set $V \subseteq \beta \times \beta$, the basis set $\text{gen}_{\mathfrak{S}}(S, V)$ for the $\mathfrak{S}$-convergence uniformity on $\alpha \to_{\mathfrak{S}} \beta$ is equal to the preimage of the basis set $\text{gen}(S, \beta, V)$ for uniform convergence on $S \to \beta$ under the product of restriction maps. That is, \[ \text{gen}_{\mathfrak{S}}(S, V) = \left(S.\text{restrict} \times S.\text{restrict}\right)^{-1} \left(\text{gen}(S, \beta, V)\right). \]

UniformOnFun.gen_mono theorem

 {𝔖} {S S' : Set α} {V V' : Set (β × β)} (hS : S' ⊆ S) (hV : V ⊆ V') : UniformOnFun.gen 𝔖 S V ⊆ UniformOnFun.gen 𝔖 S' V'

Full source

/-- `UniformOnFun.gen` is antitone in the first argument and monotone in the second. -/
protected theorem gen_mono {𝔖} {S S' : Set α} {V V' : Set (β × β)} (hS : S' ⊆ S) (hV : V ⊆ V') :
    UniformOnFun.genUniformOnFun.gen 𝔖 S V ⊆ UniformOnFun.gen 𝔖 S' V' := fun _uv h x hx => hV (h x <| hS hx)

Monotonicity of Uniform Convergence Basis Sets

Informal description

For any family of subsets $\mathfrak{S}$ of $\alpha$ and sets $S, S' \subseteq \alpha$ and $V, V' \subseteq \beta \times \beta$, if $S' \subseteq S$ and $V \subseteq V'$, then the basis set $\text{gen}_{\mathfrak{S}}(S, V)$ for the uniformity of $\mathfrak{S}$-convergence is contained in $\text{gen}_{\mathfrak{S}}(S', V')$. In other words, the set of function pairs $(f,g)$ satisfying $(f(x), g(x)) \in V$ for all $x \in S$ is contained in the set of pairs satisfying $(f(x), g(x)) \in V'$ for all $x \in S'$.

UniformOnFun.isBasis_gen theorem

 (𝔖 : Set (Set α)) (h : 𝔖.Nonempty) (h' : DirectedOn (· ⊆ ·) 𝔖) (𝓑 : FilterBasis <| β × β) :
  IsBasis (fun SV : Set α × Set (β × β) => SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓑) fun SV => UniformOnFun.gen 𝔖 SV.1 SV.2

Full source

/-- If `𝔖 : Set (Set α)` is nonempty and directed and `𝓑` is a filter basis on `β × β`, then the
family `UniformOnFun.gen 𝔖 S V` for `S ∈ 𝔖` and `V ∈ 𝓑` is a filter basis on
`(α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)`.
We will show in `has_basis_uniformity_of_basis` that, if `𝓑` is a basis for `𝓤 β`, then the
corresponding filter is the uniformity of `α →ᵤ[𝔖] β`. -/
protected theorem isBasis_gen (𝔖 : Set (Set α)) (h : 𝔖.Nonempty) (h' : DirectedOn (· ⊆ ·) 𝔖)
    (𝓑 : FilterBasis <| β × β) :
    IsBasis (fun SV : SetSet α × Set (β × β) => SV.1 ∈ 𝔖SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓑) fun SV =>
      UniformOnFun.gen 𝔖 SV.1 SV.2 :=
  ⟨h.prod 𝓑.nonempty, fun {U₁V₁ U₂V₂} h₁ h₂ =>
    let ⟨U₃, hU₃, hU₁₃, hU₂₃⟩ := h' U₁V₁.1 h₁.1 U₂V₂.1 h₂.1
    let ⟨V₃, hV₃, hV₁₂₃⟩ := 𝓑.inter_sets h₁.2 h₂.2
    ⟨⟨U₃, V₃⟩,
      ⟨⟨hU₃, hV₃⟩, fun _ H =>
        ⟨fun x hx => (hV₁₂₃ <| H x <| hU₁₃ hx).1, fun x hx => (hV₁₂₃ <| H x <| hU₂₃ hx).2⟩⟩⟩⟩

Filter Basis for Uniform $\mathfrak{S}$-Convergence

Informal description

Let $\mathfrak{S}$ be a nonempty family of subsets of $\alpha$ that is directed with respect to inclusion, and let $\mathcal{B}$ be a filter basis on $\beta \times \beta$. Then the family of sets $\text{gen}_{\mathfrak{S}}(S, V)$ for $S \in \mathfrak{S}$ and $V \in \mathcal{B}$ forms a filter basis on $(\alpha \to_{\mathfrak{S}} \beta) \times (\alpha \to_{\mathfrak{S}} \beta)$, where $\text{gen}_{\mathfrak{S}}(S, V)$ consists of all pairs $(f, g)$ such that $(f(x), g(x)) \in V$ for all $x \in S$.

UniformOnFun.uniformSpace instance

: UniformSpace (α →ᵤ[𝔖] β)

Full source

/-- Uniform structure of `𝔖`-convergence, i.e uniform convergence on the elements of `𝔖`,
declared as an instance on `α →ᵤ[𝔖] β`. It is defined as the infimum, for `S ∈ 𝔖`, of the pullback
by `S.restrict`, the map of restriction to `S`, of the uniform structure `𝒰(s, β, uβ)` on
`↥S →ᵤ β`. We will denote it `𝒱(α, β, 𝔖, uβ)`, where `uβ` is the uniform structure on `β`. -/
instance uniformSpace : UniformSpace (α →ᵤ[𝔖] β) :=
  ⨅ (s : Set α) (_ : s ∈ 𝔖),
    .comap (UniformFun.ofFun ∘ s.restrict ∘ UniformOnFun.toFun 𝔖) 𝒰(s, β, _)

Uniform Structure of 𝔖-Convergence on Function Space

Informal description

The space of functions $\alpha \to_{\mathfrak{S}} \beta$ is equipped with the uniform structure of $\mathfrak{S}$-convergence, where $\mathfrak{S}$ is a family of subsets of $\alpha$. This uniform structure is defined as the infimum, over all $S \in \mathfrak{S}$, of the pullback of the uniform structure of uniform convergence on $S \to \beta$ via the restriction map to $S$.

UniformOnFun.topologicalSpace instance

: TopologicalSpace (α →ᵤ[𝔖] β)

Full source

/-- Topology of `𝔖`-convergence, i.e uniform convergence on the elements of `𝔖`, declared as an
instance on `α →ᵤ[𝔖] β`. -/
instance topologicalSpace : TopologicalSpace (α →ᵤ[𝔖] β) :=
  𝒱(α, β, 𝔖, _).toTopologicalSpace

Topology of Uniform Convergence on a Family of Sets

Informal description

The space of functions $\alpha \to_{\mathfrak{S}} \beta$ is equipped with the topology of $\mathfrak{S}$-convergence, where $\mathfrak{S}$ is a family of subsets of $\alpha$. This topology is defined as the infimum, over all $S \in \mathfrak{S}$, of the pullback of the topology of uniform convergence on $S \to \beta$ via the restriction map to $S$.

UniformOnFun.topologicalSpace_eq theorem

 :
  UniformOnFun.topologicalSpace α β 𝔖 =
    ⨅ (s : Set α) (_ : s ∈ 𝔖),
      TopologicalSpace.induced (UniformFun.ofFun ∘ s.restrict ∘ toFun 𝔖) (UniformFun.topologicalSpace s β)

Full source

/-- The topology of `𝔖`-convergence is the infimum, for `S ∈ 𝔖`, of topology induced by the map
of `S.restrict : (α →ᵤ[𝔖] β) → (↥S →ᵤ β)` of restriction to `S`, where `↥S →ᵤ β` is endowed with
the topology of uniform convergence. -/
protected theorem topologicalSpace_eq :
    UniformOnFun.topologicalSpace α β 𝔖 =
      ⨅ (s : Set α) (_ : s ∈ 𝔖), TopologicalSpace.induced
        (UniformFun.ofFun ∘ s.restrict ∘ toFun 𝔖) (UniformFun.topologicalSpace s β) := by
  simp only [UniformOnFun.topologicalSpace, UniformSpace.toTopologicalSpace_iInf]
  rfl

Topology of $\mathfrak{S}$-Convergence as Infimum of Induced Topologies

Informal description

The topology of $\mathfrak{S}$-convergence on the function space $\alpha \to_{\mathfrak{S}} \beta$ is equal to the infimum over all sets $S \in \mathfrak{S}$ of the topology induced by the restriction map $S.\text{restrict} \colon (\alpha \to_{\mathfrak{S}} \beta) \to (S \toᵤ \beta)$, where $S \toᵤ \beta$ is equipped with the topology of uniform convergence.

UniformOnFun.hasBasis_uniformity_of_basis_aux₁ theorem

 {p : ι → Prop} {s : ι → Set (β × β)} (hb : HasBasis (𝓤 β) p s) (S : Set α) :
  (@uniformity (α →ᵤ[𝔖] β) ((UniformFun.uniformSpace S β).comap S.restrict)).HasBasis p fun i =>
    UniformOnFun.gen 𝔖 S (s i)

Full source

protected theorem hasBasis_uniformity_of_basis_aux₁ {p : ι → Prop} {s : ι → Set (β × β)}
    (hb : HasBasis (𝓤 β) p s) (S : Set α) :
    (@uniformity (α →ᵤ[𝔖] β) ((UniformFun.uniformSpace S β).comap S.restrict)).HasBasis p fun i =>
      UniformOnFun.gen 𝔖 S (s i) := by
  simp_rw [UniformOnFun.gen_eq_preimage_restrict, uniformity_comap]
  exact (UniformFun.hasBasis_uniformity_of_basis S β hb).comap _

Basis for Restricted Uniformity in $\mathfrak{S}$-Convergence Function Space

Informal description

Let $\beta$ be a uniform space with a basis $\{s(i) \mid p(i)\}$ for its uniformity $\mathcal{U}(\beta)$, indexed by a type $\iota$ with a predicate $p : \iota \to \text{Prop}$. For any subset $S \subseteq \alpha$, the uniformity on the function space $\alpha \to_{\mathfrak{S}} \beta$ (equipped with the uniform structure of $\mathfrak{S}$-convergence) restricted to $S$ has a basis consisting of the sets $\text{gen}_{\mathfrak{S}}(S, s(i))$ for $i \in \iota$ satisfying $p(i)$, where $\text{gen}_{\mathfrak{S}}(S, V) := \{(f, g) \mid \forall x \in S, (f(x), g(x)) \in V\}$.

UniformOnFun.hasBasis_uniformity_of_basis_aux₂ theorem

 (h : DirectedOn (· ⊆ ·) 𝔖) {p : ι → Prop} {s : ι → Set (β × β)} (hb : HasBasis (𝓤 β) p s) :
  DirectedOn ((fun s : Set α => (UniformFun.uniformSpace s β).comap (s.restrict : (α →ᵤ β) → s →ᵤ β)) ⁻¹'o GE.ge) 𝔖

Full source

protected theorem hasBasis_uniformity_of_basis_aux₂ (h : DirectedOn (· ⊆ ·) 𝔖) {p : ι → Prop}
    {s : ι → Set (β × β)} (hb : HasBasis (𝓤 β) p s) :
    DirectedOn
      ((fun s : Set α => (UniformFun.uniformSpace s β).comap (s.restrict : (α →ᵤ β) → s →ᵤ β)) ⁻¹'o
        GE.ge)
      𝔖 :=
  h.mono fun _ _ hst =>
    ((UniformOnFun.hasBasis_uniformity_of_basis_aux₁ α β 𝔖 hb _).le_basis_iff
          (UniformOnFun.hasBasis_uniformity_of_basis_aux₁ α β 𝔖 hb _)).mpr
      fun V hV => ⟨V, hV, UniformOnFun.gen_mono hst subset_rfl⟩

Directedness of Pullback Uniform Structures under $\mathfrak{S}$-Convergence

Informal description

Let $\mathfrak{S}$ be a family of subsets of $\alpha$ that is directed with respect to inclusion (i.e., for any $S_1, S_2 \in \mathfrak{S}$, there exists $S \in \mathfrak{S}$ such that $S_1 \subseteq S$ and $S_2 \subseteq S$). Let $\{s(i)\}_{i \in \iota}$ be a basis for the uniformity $\mathcal{U}(\beta)$ of $\beta$, indexed by a type $\iota$ with a predicate $p : \iota \to \text{Prop}$. Then, the family of uniform structures obtained by pulling back (via restriction) the uniform structures of uniform convergence on each $S \in \mathfrak{S}$ is directed with respect to the reverse inclusion order on $\mathfrak{S}$.

UniformOnFun.hasBasis_uniformity_of_basis theorem

 (h : 𝔖.Nonempty) (h' : DirectedOn (· ⊆ ·) 𝔖) {p : ι → Prop} {s : ι → Set (β × β)} (hb : HasBasis (𝓤 β) p s) :
  (𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun Si : Set α × ι => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => UniformOnFun.gen 𝔖 Si.1 (s Si.2)

Full source

/-- If `𝔖 : Set (Set α)` is nonempty and directed and `𝓑` is a filter basis of `𝓤 β`, then the
uniformity of `α →ᵤ[𝔖] β` admits the family `{(f, g) | ∀ x ∈ S, (f x, g x) ∈ V}` for `S ∈ 𝔖` and
`V ∈ 𝓑` as a filter basis. -/
protected theorem hasBasis_uniformity_of_basis (h : 𝔖.Nonempty) (h' : DirectedOn (· ⊆ ·) 𝔖)
    {p : ι → Prop} {s : ι → Set (β × β)} (hb : HasBasis (𝓤 β) p s) :
    (𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun Si : SetSet α × ι => Si.1 ∈ 𝔖Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
      UniformOnFun.gen 𝔖 Si.1 (s Si.2) := by
  simp only [iInf_uniformity]
  exact
    hasBasis_biInf_of_directed h (fun S => UniformOnFun.genUniformOnFun.gen 𝔖 S ∘ s) _
      (fun S _hS => UniformOnFun.hasBasis_uniformity_of_basis_aux₁ α β 𝔖 hb S)
      (UniformOnFun.hasBasis_uniformity_of_basis_aux₂ α β 𝔖 h' hb)

Basis for Uniformity of $\mathfrak{S}$-Convergence in Terms of Basis for $\mathcal{U}(\beta)$

Informal description

Let $\alpha$ and $\beta$ be types, with $\beta$ equipped with a uniform structure. Let $\mathfrak{S}$ be a nonempty family of subsets of $\alpha$ that is directed under inclusion. Suppose $\{s(i)\}_{i \in \iota}$ is a basis for the uniformity $\mathcal{U}(\beta)$ of $\beta$, indexed by a type $\iota$ with a predicate $p : \iota \to \text{Prop}$. Then the uniformity $\mathcal{U}(\alpha \to_{\mathfrak{S}} \beta)$ on the space of functions $\alpha \to_{\mathfrak{S}} \beta$ (equipped with the uniform structure of $\mathfrak{S}$-convergence) has a basis consisting of sets of the form: \[ \text{gen}_{\mathfrak{S}}(S, s(i)) := \{(f,g) \mid \forall x \in S, (f(x), g(x)) \in s(i)\} \] for pairs $(S, i) \in \mathfrak{S} \times \iota$ where $S \in \mathfrak{S}$ and $p(i)$ holds.

UniformOnFun.hasBasis_uniformity theorem

 (h : 𝔖.Nonempty) (h' : DirectedOn (· ⊆ ·) 𝔖) :
  (𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun SV : Set α × Set (β × β) => SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓤 β) fun SV =>
    UniformOnFun.gen 𝔖 SV.1 SV.2

Full source

/-- If `𝔖 : Set (Set α)` is nonempty and directed, then the uniformity of `α →ᵤ[𝔖] β` admits the
family `{(f, g) | ∀ x ∈ S, (f x, g x) ∈ V}` for `S ∈ 𝔖` and `V ∈ 𝓤 β` as a filter basis. -/
protected theorem hasBasis_uniformity (h : 𝔖.Nonempty) (h' : DirectedOn (· ⊆ ·) 𝔖) :
    (𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun SV : SetSet α × Set (β × β) => SV.1 ∈ 𝔖SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓤 β) fun SV =>
      UniformOnFun.gen 𝔖 SV.1 SV.2 :=
  UniformOnFun.hasBasis_uniformity_of_basis α β 𝔖 h h' (𝓤 β).basis_sets

Basis for Uniformity of $\mathfrak{S}$-Convergence in Terms of $\mathcal{U}(\beta)$

Informal description

Let $\mathfrak{S}$ be a nonempty family of subsets of $\alpha$ that is directed under inclusion. Then the uniformity $\mathcal{U}(\alpha \to_{\mathfrak{S}} \beta)$ on the space of functions $\alpha \to_{\mathfrak{S}} \beta$ has a basis consisting of sets of the form: \[ \{(f,g) \mid \forall x \in S, (f(x), g(x)) \in V\} \] for $S \in \mathfrak{S}$ and $V$ in the uniformity $\mathcal{U}(\beta)$ of $\beta$.

UniformOnFun.hasBasis_uniformity_of_covering_of_basis theorem

 {ι ι' : Type*} [Nonempty ι] {t : ι → Set α} {p : ι' → Prop} {V : ι' → Set (β × β)} (ht : ∀ i, t i ∈ 𝔖)
  (hdir : Directed (· ⊆ ·) t) (hex : ∀ s ∈ 𝔖, ∃ i, s ⊆ t i) (hb : HasBasis (𝓤 β) p V) :
  (𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun i : ι × ι' ↦ p i.2) fun i ↦ UniformOnFun.gen 𝔖 (t i.1) (V i.2)

Full source

/-- Let `t i` be a nonempty directed subfamily of `𝔖`
such that every `s ∈ 𝔖` is included in some `t i`.
Let `V` bounded by `p` be a basis of entourages of `β`.

Then `UniformOnFun.gen 𝔖 (t i) (V j)` bounded by `p j` is a basis of entourages of `α →ᵤ[𝔖] β`. -/
protected theorem hasBasis_uniformity_of_covering_of_basis {ι ι' : Type*} [Nonempty ι]
    {t : ι → Set α} {p : ι' → Prop} {V : ι' → Set (β × β)} (ht : ∀ i, t i ∈ 𝔖)
    (hdir : Directed (· ⊆ ·) t) (hex : ∀ s ∈ 𝔖, ∃ i, s ⊆ t i) (hb : HasBasis (𝓤 β) p V) :
    (𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun i : ι × ι' ↦ p i.2) fun i ↦
      UniformOnFun.gen 𝔖 (t i.1) (V i.2) := by
  have hne : 𝔖.Nonempty := (range_nonempty t).mono (range_subset_iff.2 ht)
  have hd : DirectedOn (· ⊆ ·) 𝔖 := fun s₁ hs₁ s₂ hs₂ ↦ by
    rcases hex s₁ hs₁, hex s₂ hs₂ with ⟨⟨i₁, his₁⟩, i₂, his₂⟩
    rcases hdir i₁ i₂ with ⟨i, hi₁, hi₂⟩
    exact ⟨t i, ht _, his₁.trans hi₁, his₂.trans hi₂⟩
  refine (UniformOnFun.hasBasis_uniformity_of_basis α β 𝔖 hne hd hb).to_hasBasis
    (fun ⟨s, i'⟩ ⟨hs, hi'⟩ ↦ ?_) fun ⟨i, i'⟩ hi' ↦ ⟨(t i, i'), ⟨ht i, hi'⟩, Subset.rfl⟩
  rcases hex s hs with ⟨i, hi⟩
  exact ⟨(i, i'), hi', UniformOnFun.gen_mono hi Subset.rfl⟩

Basis for Uniformity of $\mathfrak{S}$-Convergence via Directed Covering and Uniformity Basis

Informal description

Let $\alpha$ and $\beta$ be types, with $\beta$ equipped with a uniform structure. Let $\mathfrak{S}$ be a family of subsets of $\alpha$ and let $\{t_i\}_{i \in \iota}$ be a nonempty directed family in $\mathfrak{S}$ such that every $s \in \mathfrak{S}$ is contained in some $t_i$. Suppose $\{V_j\}_{j \in \iota'}$ is a basis for the uniformity $\mathcal{U}(\beta)$, indexed by $\iota'$ with a predicate $p : \iota' \to \text{Prop}$. Then the uniformity $\mathcal{U}(\alpha \to_{\mathfrak{S}} \beta)$ of $\mathfrak{S}$-convergence has a basis consisting of the sets: \[ \text{gen}_{\mathfrak{S}}(t_i, V_j) := \{(f,g) \mid \forall x \in t_i, (f(x), g(x)) \in V_j\} \] for pairs $(i,j) \in \iota \times \iota'$ where $p(j)$ holds.

UniformOnFun.hasAntitoneBasis_uniformity theorem

 {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)] {t : ι → Set α} {V : ι → Set (β × β)} (ht : ∀ n, t n ∈ 𝔖)
  (hmono : Monotone t) (hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n) (hb : HasAntitoneBasis (𝓤 β) V) :
  (𝓤 (α →ᵤ[𝔖] β)).HasAntitoneBasis fun n ↦ UniformOnFun.gen 𝔖 (t n) (V n)

Full source

/-- If `t n` is a monotone sequence of sets in `𝔖`
such that each `s ∈ 𝔖` is included in some `t n`
and `V n` is an antitone basis of entourages of `β`,
then `UniformOnFun.gen 𝔖 (t n) (V n)` is an antitone basis of entourages of `α →ᵤ[𝔖] β`. -/
protected theorem hasAntitoneBasis_uniformity {ι : Type*} [Preorder ι] [IsDirected ι (· ≤ ·)]
    {t : ι → Set α} {V : ι → Set (β × β)}
    (ht : ∀ n, t n ∈ 𝔖) (hmono : Monotone t) (hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n)
    (hb : HasAntitoneBasis (𝓤 β) V) :
    (𝓤 (α →ᵤ[𝔖] β)).HasAntitoneBasis fun n ↦ UniformOnFun.gen 𝔖 (t n) (V n) := by
  have := hb.nonempty
  refine ⟨(UniformOnFun.hasBasis_uniformity_of_covering_of_basis 𝔖
    ht hmono.directed_le hex hb.1).to_hasBasis ?_ fun i _ ↦ ⟨(i, i), trivial, Subset.rfl⟩, ?_⟩
  · rintro ⟨k, l⟩ -
    rcases directed_of (· ≤ ·) k l with ⟨n, hkn, hln⟩
    exact ⟨n, trivial, UniformOnFun.gen_mono (hmono hkn) (hb.2 <| hln)⟩
  · exact fun k l h ↦ UniformOnFun.gen_mono (hmono h) (hb.2 h)

Antitone Basis for Uniformity of $\mathfrak{S}$-Convergence via Monotone Covering and Antitone Uniformity Basis

Informal description

Let $\alpha$ and $\beta$ be types, with $\beta$ equipped with a uniform structure. Let $\mathfrak{S}$ be a family of subsets of $\alpha$. Suppose $\{t_n\}_{n \in \iota}$ is a monotone sequence of sets in $\mathfrak{S}$ indexed by a directed preorder $\iota$ such that every $s \in \mathfrak{S}$ is contained in some $t_n$, and $\{V_n\}_{n \in \iota}$ is an antitone basis of entourages for the uniformity $\mathcal{U}(\beta)$. Then the sets $\text{gen}_{\mathfrak{S}}(t_n, V_n) := \{(f,g) \mid \forall x \in t_n, (f(x), g(x)) \in V_n\}$ form an antitone basis for the uniformity $\mathcal{U}(\alpha \to_{\mathfrak{S}} \beta)$ of $\mathfrak{S}$-convergence.

UniformOnFun.isCountablyGenerated_uniformity theorem

 [IsCountablyGenerated (𝓤 β)] {t : ℕ → Set α} (ht : ∀ n, t n ∈ 𝔖) (hmono : Monotone t) (hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n) :
  IsCountablyGenerated (𝓤 (α →ᵤ[𝔖] β))

Full source

protected theorem isCountablyGenerated_uniformity [IsCountablyGenerated (𝓤 β)] {t : ℕ → Set α}
    (ht : ∀ n, t n ∈ 𝔖) (hmono : Monotone t) (hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n) :
    IsCountablyGenerated (𝓤 (α →ᵤ[𝔖] β)) :=
  let ⟨_V, hV⟩ := exists_antitone_basis (𝓤 β)
  (UniformOnFun.hasAntitoneBasis_uniformity 𝔖 ht hmono hex hV).isCountablyGenerated

Countable Generation of Uniformity for $\mathfrak{S}$-Convergence Function Space

Informal description

Let $\alpha$ and $\beta$ be types, with $\beta$ equipped with a uniform structure whose uniformity $\mathcal{U}(\beta)$ has a countable basis. Let $\mathfrak{S}$ be a family of subsets of $\alpha$ and $\{t_n\}_{n \in \mathbb{N}}$ be a monotone sequence of sets in $\mathfrak{S}$ such that every $S \in \mathfrak{S}$ is contained in some $t_n$. Then the uniformity $\mathcal{U}(\alpha \to_{\mathfrak{S}} \beta)$ of $\mathfrak{S}$-convergence is countably generated.

UniformOnFun.hasBasis_nhds_of_basis theorem

 (f : α →ᵤ[𝔖] β) (h : 𝔖.Nonempty) (h' : DirectedOn (· ⊆ ·) 𝔖) {p : ι → Prop} {s : ι → Set (β × β)}
  (hb : HasBasis (𝓤 β) p s) :
  (𝓝 f).HasBasis (fun Si : Set α × ι => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => {g | (g, f) ∈ UniformOnFun.gen 𝔖 Si.1 (s Si.2)}

Full source

/-- For `f : α →ᵤ[𝔖] β`, where `𝔖 : Set (Set α)` is nonempty and directed, `𝓝 f` admits the
family `{g | ∀ x ∈ S, (f x, g x) ∈ V}` for `S ∈ 𝔖` and `V ∈ 𝓑` as a filter basis, for any basis
`𝓑` of `𝓤 β`. -/
protected theorem hasBasis_nhds_of_basis (f : α →ᵤ[𝔖] β) (h : 𝔖.Nonempty)
    (h' : DirectedOn (· ⊆ ·) 𝔖) {p : ι → Prop} {s : ι → Set (β × β)} (hb : HasBasis (𝓤 β) p s) :
    (𝓝 f).HasBasis (fun Si : SetSet α × ι => Si.1 ∈ 𝔖Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
      { g | (g, f) ∈ UniformOnFun.gen 𝔖 Si.1 (s Si.2) } :=
  letI : UniformSpace (α → β) := UniformOnFun.uniformSpace α β 𝔖
  nhds_basis_uniformity (UniformOnFun.hasBasis_uniformity_of_basis α β 𝔖 h h' hb)

Basis for Neighborhood Filter in $\mathfrak{S}$-Convergence Function Space

Informal description

Let $\alpha$ and $\beta$ be types, with $\beta$ equipped with a uniform structure. Let $\mathfrak{S}$ be a nonempty family of subsets of $\alpha$ that is directed under inclusion. Given a function $f \in \alpha \to_{\mathfrak{S}} \beta$ and a basis $\{s(i)\}_{i \in \iota}$ for the uniformity $\mathcal{U}(\beta)$ indexed by a type $\iota$ with a predicate $p : \iota \to \text{Prop}$, the neighborhood filter $\mathcal{N}(f)$ has a basis consisting of sets of the form: \[ \{g \mid \forall x \in S, (g(x), f(x)) \in s(i)\} \] for pairs $(S, i) \in \mathfrak{S} \times \iota$ where $S \in \mathfrak{S}$ and $p(i)$ holds.

UniformOnFun.hasBasis_nhds theorem

 (f : α →ᵤ[𝔖] β) (h : 𝔖.Nonempty) (h' : DirectedOn (· ⊆ ·) 𝔖) :
  (𝓝 f).HasBasis (fun SV : Set α × Set (β × β) => SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓤 β) fun SV =>
    {g | (g, f) ∈ UniformOnFun.gen 𝔖 SV.1 SV.2}

Full source

/-- For `f : α →ᵤ[𝔖] β`, where `𝔖 : Set (Set α)` is nonempty and directed, `𝓝 f` admits the
family `{g | ∀ x ∈ S, (f x, g x) ∈ V}` for `S ∈ 𝔖` and `V ∈ 𝓤 β` as a filter basis. -/
protected theorem hasBasis_nhds (f : α →ᵤ[𝔖] β) (h : 𝔖.Nonempty) (h' : DirectedOn (· ⊆ ·) 𝔖) :
    (𝓝 f).HasBasis (fun SV : SetSet α × Set (β × β) => SV.1 ∈ 𝔖SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓤 β) fun SV =>
      { g | (g, f) ∈ UniformOnFun.gen 𝔖 SV.1 SV.2 } :=
  UniformOnFun.hasBasis_nhds_of_basis α β 𝔖 f h h' (Filter.basis_sets _)

Basis for Neighborhood Filter in Function Space with Uniform $\mathfrak{S}$-Convergence

Informal description

Let $\alpha$ and $\beta$ be types, with $\beta$ equipped with a uniform structure. Let $\mathfrak{S}$ be a nonempty family of subsets of $\alpha$ that is directed under inclusion. For any function $f \in \alpha \to_{\mathfrak{S}} \beta$, the neighborhood filter $\mathcal{N}(f)$ has a basis consisting of sets of the form: \[ \{g \mid \forall x \in S, (f(x), g(x)) \in V\} \] where $S \in \mathfrak{S}$ and $V$ belongs to the uniformity $\mathcal{U}(\beta)$ of $\beta$.

UniformOnFun.uniformContinuous_restrict theorem

(h : s ∈ 𝔖) : UniformContinuous (UniformFun.ofFun ∘ (s.restrict : (α → β) → s → β) ∘ toFun 𝔖)

Full source

/-- If `S ∈ 𝔖`, then the restriction to `S` is a uniformly continuous map from `α →ᵤ[𝔖] β` to
`↥S →ᵤ β`. -/
protected theorem uniformContinuous_restrict (h : s ∈ 𝔖) :
    UniformContinuous (UniformFun.ofFunUniformFun.ofFun ∘ (s.restrict : (α → β) → s → β) ∘ toFun 𝔖) := by
  change _ ≤ _
  simp only [UniformOnFun.uniformSpace, map_le_iff_le_comap, iInf_uniformity]
  exact iInf₂_le s h

Uniform Continuity of Function Restriction in $\mathfrak{S}$-Convergence

Informal description

For any set $s$ in the family $\mathfrak{S}$ of subsets of $\alpha$, the restriction map from $\alpha \to_{\mathfrak{S}} \beta$ to $s \to \beta$ is uniformly continuous, where $\alpha \to_{\mathfrak{S}} \beta$ is equipped with the uniform structure of $\mathfrak{S}$-convergence and $s \to \beta$ is equipped with the uniform structure of uniform convergence.

UniformOnFun.uniformity_eq_of_basis theorem

 {ι : Sort*} {p : ι → Prop} {V : ι → Set (β × β)} (h : (𝓤 β).HasBasis p V) :
  𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ (i) (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))

Full source

/-- A version of `UniformOnFun.hasBasis_uniformity_of_basis`
with weaker conclusion and weaker assumptions.

We make no assumptions about the set `𝔖`
but conclude only that the uniformity is equal to some indexed infimum. -/
protected theorem uniformity_eq_of_basis {ι : Sort*} {p : ι → Prop} {V : ι → Set (β × β)}
    (h : (𝓤 β).HasBasis p V) :
    𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ (i) (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)) := by
  simp_rw [iInf_uniformity, uniformity_comap,
    (UniformFun.hasBasis_uniformity_of_basis _ _ h).eq_biInf, comap_iInf, comap_principal,
    Function.comp_apply, UniformFun.gen, Subtype.forall, UniformOnFun.gen, preimage_setOf_eq,
    Prod.map_fst, Prod.map_snd, Function.comp_apply, UniformFun.toFun_ofFun, restrict_apply]

Basis Characterization of Uniformity for $\mathfrak{S}$-Convergence

Informal description

Let $\beta$ be a uniform space with a basis $\{V_i\}_{i \in \iota}$ for its uniformity $\mathcal{U}(\beta)$, indexed by a type $\iota$ with a predicate $p : \iota \to \text{Prop}$. Then the uniformity $\mathcal{U}(\alpha \to_{\mathfrak{S}} \beta)$ of $\mathfrak{S}$-convergence on the function space $\alpha \to_{\mathfrak{S}} \beta$ is equal to the infimum over all $s \in \mathfrak{S}$ and all $i \in \iota$ with $p(i)$ of the principal filters generated by the sets $\text{gen}_{\mathfrak{S}}(s, V_i) := \{(f, g) \mid \forall x \in s, (f(x), g(x)) \in V_i\}$.

UniformOnFun.uniformity_eq theorem

: 𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V)

Full source

protected theorem uniformity_eq : 𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V) :=
  UniformOnFun.uniformity_eq_of_basis _ _ (𝓤 β).basis_sets

Characterization of Uniformity for $\mathfrak{S}$-Convergence on Function Space

Informal description

The uniformity $\mathcal{U}(\alpha \to_{\mathfrak{S}} \beta)$ of $\mathfrak{S}$-convergence on the function space $\alpha \to_{\mathfrak{S}} \beta$ is equal to the infimum over all sets $s \in \mathfrak{S}$ and all entourages $V$ in the uniformity $\mathcal{U}(\beta)$ of the principal filters generated by the sets $\text{gen}_{\mathfrak{S}}(s, V) := \{(f, g) \mid \forall x \in s, (f(x), g(x)) \in V\}$.

UniformOnFun.gen_mem_uniformity theorem

(hs : s ∈ 𝔖) {V : Set (β × β)} (hV : V ∈ 𝓤 β) : UniformOnFun.gen 𝔖 s V ∈ 𝓤 (α →ᵤ[𝔖] β)

Full source

protected theorem gen_mem_uniformity (hs : s ∈ 𝔖) {V : Set (β × β)} (hV : V ∈ 𝓤 β) :
    UniformOnFun.genUniformOnFun.gen 𝔖 s V ∈ 𝓤 (α →ᵤ[𝔖] β) := by
  rw [UniformOnFun.uniformity_eq]
  apply_rules [mem_iInf_of_mem, mem_principal_self]

Basis Sets for $\mathfrak{S}$-Convergence Uniformity Belong to Uniformity

Informal description

For any set $s$ in the family $\mathfrak{S}$ of subsets of $\alpha$ and any entourage $V$ in the uniformity $\mathcal{U}(\beta)$ of $\beta$, the set $\text{gen}_{\mathfrak{S}}(s, V) := \{(f, g) \mid \forall x \in s, (f(x), g(x)) \in V\}$ belongs to the uniformity $\mathcal{U}(\alpha \to_{\mathfrak{S}} \beta)$ of $\mathfrak{S}$-convergence on the function space $\alpha \to_{\mathfrak{S}} \beta$.

UniformOnFun.nhds_eq_of_basis theorem

 {ι : Sort*} {p : ι → Prop} {V : ι → Set (β × β)} (h : (𝓤 β).HasBasis p V) (f : α →ᵤ[𝔖] β) :
  𝓝 f = ⨅ s ∈ 𝔖, ⨅ (i) (_ : p i), 𝓟 {g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V i}

Full source

/-- A version of `UniformOnFun.hasBasis_nhds_of_basis`
with weaker conclusion and weaker assumptions.

We make no assumptions about the set `𝔖`
but conclude only that the neighbourhoods filter is equal to some indexed infimum. -/
protected theorem nhds_eq_of_basis {ι : Sort*} {p : ι → Prop} {V : ι → Set (β × β)}
    (h : (𝓤 β).HasBasis p V) (f : α →ᵤ[𝔖] β) :
    𝓝 f = ⨅ s ∈ 𝔖, ⨅ (i) (_ : p i), 𝓟 {g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V i} := by
  simp_rw [nhds_eq_comap_uniformity, UniformOnFun.uniformity_eq_of_basis _ _ h, comap_iInf,
    comap_principal, UniformOnFun.gen, preimage_setOf_eq]

Characterization of Neighborhood Filter in $\mathfrak{S}$-Convergence via Basis

Informal description

Let $\beta$ be a uniform space with a basis $\{V_i\}_{i \in \iota}$ for its uniformity $\mathcal{U}(\beta)$, indexed by a type $\iota$ with a predicate $p : \iota \to \text{Prop}$. For any function $f \in \alpha \to_{\mathfrak{S}} \beta$ equipped with the topology of $\mathfrak{S}$-convergence, the neighborhood filter $\mathcal{N}(f)$ is equal to the infimum over all $s \in \mathfrak{S}$ and all $i \in \iota$ with $p(i)$ of the principal filters generated by the sets $\{g \mid \forall x \in s, (f(x), g(x)) \in V_i\}$.

UniformOnFun.nhds_eq theorem

 (f : α →ᵤ[𝔖] β) : 𝓝 f = ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 {g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V}

Full source

protected theorem nhds_eq (f : α →ᵤ[𝔖] β) :
    𝓝 f = ⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 {g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V} :=
  UniformOnFun.nhds_eq_of_basis _ _ (𝓤 β).basis_sets f

Characterization of Neighborhood Filter in Uniform Convergence on a Family of Sets

Informal description

For any function $f$ in the space $\alpha \to_{\mathfrak{S}} \beta$ equipped with the topology of uniform convergence on a family $\mathfrak{S}$ of subsets of $\alpha$, the neighborhood filter $\mathcal{N}(f)$ is equal to the infimum over all $s \in \mathfrak{S}$ and all entourages $V$ in the uniformity $\mathcal{U}(\beta)$ of the principal filters generated by the sets $\{g \mid \forall x \in s, (f(x), g(x)) \in V\}$.

UniformOnFun.gen_mem_nhds theorem

 (f : α →ᵤ[𝔖] β) (hs : s ∈ 𝔖) {V : Set (β × β)} (hV : V ∈ 𝓤 β) : {g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V} ∈ 𝓝 f

Full source

protected theorem gen_mem_nhds (f : α →ᵤ[𝔖] β) (hs : s ∈ 𝔖) {V : Set (β × β)} (hV : V ∈ 𝓤 β) :
    {g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V}{g | ∀ x ∈ s, (toFun 𝔖 f x, toFun 𝔖 g x) ∈ V} ∈ 𝓝 f := by
  rw [UniformOnFun.nhds_eq]
  apply_rules [mem_iInf_of_mem, mem_principal_self]

Neighborhood Characterization in Uniform $\mathfrak{S}$-Convergence

Informal description

For any function $f \in \alpha \to_{\mathfrak{S}} \beta$ equipped with the topology of $\mathfrak{S}$-convergence, if $s \in \mathfrak{S}$ and $V$ is an entourage in the uniformity of $\beta$, then the set $\{g \mid \forall x \in s, (f(x), g(x)) \in V\}$ is a neighborhood of $f$.

UniformOnFun.uniformContinuous_ofUniformFun theorem

: UniformContinuous fun f : α →ᵤ β ↦ ofFun 𝔖 (UniformFun.toFun f)

Full source

theorem uniformContinuous_ofUniformFun :
    UniformContinuous fun f : α →ᵤ β ↦ ofFun 𝔖 (UniformFun.toFun f) := by
  simp only [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf, tendsto_principal,
    (UniformFun.hasBasis_uniformity _ _).eventually_iff]
  exact fun _ _ U hU ↦ ⟨U, hU, fun f hf x _ ↦ hf x⟩

Uniform Continuity of the Embedding from Uniform Convergence to $\mathfrak{S}$-Convergence

Informal description

The map that converts a function $f \in \alpha \toᵤ \beta$ (with the uniform structure of uniform convergence) to its counterpart in $\alpha \to_{\mathfrak{S}} \beta$ (with the uniform structure of $\mathfrak{S}$-convergence) is uniformly continuous.

UniformOnFun.uniformEquivUniformFun definition

(h : univ ∈ 𝔖) : (α →ᵤ[𝔖] β) ≃ᵤ (α →ᵤ β)

Full source

/-- The uniformity on `α →ᵤ[𝔖] β` is the same as the uniformity on `α →ᵤ β`,
provided that `Set.univ ∈ 𝔖`.

Here we formulate it as a `UniformEquiv`. -/
def uniformEquivUniformFun (h : univuniv ∈ 𝔖) : (α →ᵤ[𝔖] β) ≃ᵤ (α →ᵤ β) where
  toFun f := UniformFun.ofFun <| toFun _ f
  invFun f := ofFun _ <| UniformFun.toFun f
  left_inv _ := rfl
  right_inv _ := rfl
  uniformContinuous_toFun := by
    simp only [UniformContinuous, (UniformFun.hasBasis_uniformity _ _).tendsto_right_iff]
    intro U hU
    filter_upwards [UniformOnFun.gen_mem_uniformity _ _ h hU] with f hf x using hf x (mem_univ _)
  uniformContinuous_invFun := uniformContinuous_ofUniformFun _ _

Uniform equivalence between $\mathfrak{S}$-convergence and uniform convergence

Informal description

Given a uniform space $\beta$ and a family $\mathfrak{S}$ of subsets of $\alpha$ that includes the entire set $\alpha$, there is a uniform equivalence between the space $\alpha \to_{\mathfrak{S}} \beta$ of functions with the uniform structure of $\mathfrak{S}$-convergence and the space $\alpha \toᵤ \beta$ of functions with the uniform structure of uniform convergence. This equivalence is given by the identity map on functions, and both the forward and inverse maps are uniformly continuous.

UniformOnFun.mono theorem

 ⦃u₁ u₂ : UniformSpace γ⦄ (hu : u₁ ≤ u₂) ⦃𝔖₁ 𝔖₂ : Set (Set α)⦄ (h𝔖 : 𝔖₂ ⊆ 𝔖₁) : 𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂)

Full source

/-- Let `u₁`, `u₂` be two uniform structures on `γ` and `𝔖₁ 𝔖₂ : Set (Set α)`. If `u₁ ≤ u₂` and
`𝔖₂ ⊆ 𝔖₁` then `𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂)`. -/
protected theorem mono ⦃u₁ u₂ : UniformSpace γ⦄ (hu : u₁ ≤ u₂) ⦃𝔖₁ 𝔖₂ : Set (Set α)⦄
    (h𝔖 : 𝔖₂ ⊆ 𝔖₁) : 𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂) :=
  calc
    𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₁) := iInf_le_iInf_of_subset h𝔖
    _ ≤ 𝒱(α, γ, 𝔖₂, u₂) := iInf₂_mono fun _i _hi => UniformSpace.comap_mono <| UniformFun.mono hu

Monotonicity of Uniform Convergence Structure with Respect to Uniformity and Family of Sets

Informal description

Let $\gamma$ be a type equipped with two uniform structures $u_1$ and $u_2$ such that $u_1 \leq u_2$, and let $\mathfrak{S}_1$ and $\mathfrak{S}_2$ be families of subsets of $\alpha$ with $\mathfrak{S}_2 \subseteq \mathfrak{S}_1$. Then the uniform structure $\mathcal{V}(\alpha, \gamma, \mathfrak{S}_1, u_1)$ of $\mathfrak{S}_1$-convergence on the function space $\alpha \to_{\mathfrak{S}_1} \gamma$ is finer than the uniform structure $\mathcal{V}(\alpha, \gamma, \mathfrak{S}_2, u_2)$ of $\mathfrak{S}_2$-convergence on $\alpha \to_{\mathfrak{S}_2} \gamma$.

UniformOnFun.uniformContinuous_eval_of_mem theorem

{x : α} (hxs : x ∈ s) (hs : s ∈ 𝔖) : UniformContinuous ((Function.eval x : (α → β) → β) ∘ toFun 𝔖)

Full source

/-- If `x : α` is in some `S ∈ 𝔖`, then evaluation at `x` is uniformly continuous on
`α →ᵤ[𝔖] β`. -/
theorem uniformContinuous_eval_of_mem {x : α} (hxs : x ∈ s) (hs : s ∈ 𝔖) :
    UniformContinuous ((Function.eval x : (α → β) → β) ∘ toFun 𝔖) :=
  (UniformFun.uniformContinuous_eval β (⟨x, hxs⟩ : s)).comp
    (UniformOnFun.uniformContinuous_restrict α β 𝔖 hs)

Uniform Continuity of Evaluation at Points in $\mathfrak{S}$ for $\mathfrak{S}$-Convergence

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a uniform structure, and let $\mathfrak{S}$ be a family of subsets of $\alpha$. For any $x \in \alpha$ that belongs to some set $s \in \mathfrak{S}$, the evaluation map at $x$ is uniformly continuous from the function space $\alpha \to_{\mathfrak{S}} \beta$ (equipped with the uniform structure of $\mathfrak{S}$-convergence) to $\beta$.

UniformOnFun.uniformContinuous_eval_of_mem_sUnion theorem

{x : α} (hx : x ∈ ⋃₀ 𝔖) : UniformContinuous ((Function.eval x : (α → β) → β) ∘ toFun 𝔖)

Full source

theorem uniformContinuous_eval_of_mem_sUnion {x : α} (hx : x ∈ ⋃₀ 𝔖) :
    UniformContinuous ((Function.eval x : (α → β) → β) ∘ toFun 𝔖) :=
  let ⟨_s, hs, hxs⟩ := hx
  uniformContinuous_eval_of_mem _ _ hxs hs

Uniform Continuity of Evaluation at Points in the Union of $\mathfrak{S}$ for $\mathfrak{S}$-Convergence

Informal description

For any point $x \in \alpha$ that belongs to the union of the family $\mathfrak{S}$ of subsets of $\alpha$, the evaluation map at $x$ is uniformly continuous from the function space $\alpha \to_{\mathfrak{S}} \beta$ (equipped with the uniform structure of $\mathfrak{S}$-convergence) to $\beta$.

UniformOnFun.uniformContinuous_eval theorem

(h : ⋃₀ 𝔖 = univ) (x : α) : UniformContinuous ((Function.eval x : (α → β) → β) ∘ toFun 𝔖)

Full source

theorem uniformContinuous_eval (h : ⋃₀ 𝔖 = univ) (x : α) :
    UniformContinuous ((Function.eval x : (α → β) → β) ∘ toFun 𝔖) :=
  uniformContinuous_eval_of_mem_sUnion _ _ <| h.symm ▸ mem_univ _

Uniform Continuity of Evaluation for Total Covering $\mathfrak{S}$ in $\mathfrak{S}$-Convergence

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a uniform structure, and let $\mathfrak{S}$ be a family of subsets of $\alpha$ whose union covers $\alpha$ (i.e., $\bigcup_{S \in \mathfrak{S}} S = \alpha$). Then for any point $x \in \alpha$, the evaluation map at $x$ is uniformly continuous from the function space $\alpha \to_{\mathfrak{S}} \beta$ (equipped with the uniform structure of $\mathfrak{S}$-convergence) to $\beta$.

UniformOnFun.iInf_eq theorem

{u : ι → UniformSpace γ} : 𝒱(α, γ, 𝔖, ⨅ i, u i) = ⨅ i, 𝒱(α, γ, 𝔖, u i)

Full source

/-- If `u` is a family of uniform structures on `γ`, then
`𝒱(α, γ, 𝔖, (⨅ i, u i)) = ⨅ i, 𝒱(α, γ, 𝔖, u i)`. -/
protected theorem iInf_eq {u : ι → UniformSpace γ} :
    𝒱(α, γ, 𝔖, ⨅ i, u i) = ⨅ i, 𝒱(α, γ, 𝔖, u i) := by
  simp_rw [UniformOnFun.uniformSpace, UniformFun.iInf_eq, UniformSpace.comap_iInf]
  rw [iInf_comm]
  exact iInf_congr fun s => iInf_comm

Infimum Commutes with Uniform $\mathfrak{S}$-Convergence Structure: $\mathcal{V}(\alpha, \gamma, \mathfrak{S}, \bigsqcap_i u_i) = \bigsqcap_i \mathcal{V}(\alpha, \gamma, \mathfrak{S}, u_i)$

Informal description

For any family of uniform structures $\{u_i\}_{i \in \iota}$ on a type $\gamma$, the uniform structure of $\mathfrak{S}$-convergence on $\alpha \to_{\mathfrak{S}} \gamma$ with respect to the infimum uniform structure $\bigsqcap_i u_i$ is equal to the infimum of the uniform structures of $\mathfrak{S}$-convergence on $\alpha \to_{\mathfrak{S}} \gamma$ with respect to each $u_i$. That is, \[ \mathcal{V}(\alpha, \gamma, \mathfrak{S}, \bigsqcap_i u_i) = \bigsqcap_i \mathcal{V}(\alpha, \gamma, \mathfrak{S}, u_i). \]

UniformOnFun.inf_eq theorem

 {u₁ u₂ : UniformSpace γ} : 𝒱(α, γ, 𝔖, u₁ ⊓ u₂) = 𝒱(α, γ, 𝔖, u₁) ⊓ 𝒱(α, γ, 𝔖, u₂)

Full source

/-- If `u₁` and `u₂` are two uniform structures on `γ`, then
`𝒱(α, γ, 𝔖, u₁ ⊓ u₂) = 𝒱(α, γ, 𝔖, u₁) ⊓ 𝒱(α, γ, 𝔖, u₂)`. -/
protected theorem inf_eq {u₁ u₂ : UniformSpace γ} :
    𝒱(α, γ, 𝔖, u₁ ⊓ u₂) = 𝒱(α, γ, 𝔖, u₁)𝒱(α, γ, 𝔖, u₁) ⊓ 𝒱(α, γ, 𝔖, u₂) := by
  rw [inf_eq_iInf, inf_eq_iInf, UniformOnFun.iInf_eq]
  refine iInf_congr fun i => ?_
  cases i <;> rfl

Infimum of Uniform Structures Commutes with $\mathfrak{S}$-Convergence: $\mathcal{V}(\alpha, \gamma, \mathfrak{S}, u₁ \sqcap u₂) = \mathcal{V}(\alpha, \gamma, \mathfrak{S}, u₁) \sqcap \mathcal{V}(\alpha, \gamma, \mathfrak{S}, u₂)$

Informal description

For any two uniform structures $u₁$ and $u₂$ on a type $\gamma$, the uniform structure of $\mathfrak{S}$-convergence on the function space $\alpha \to_{\mathfrak{S}} \gamma$ with respect to the infimum $u₁ \sqcap u₂$ is equal to the infimum of the uniform structures of $\mathfrak{S}$-convergence with respect to $u₁$ and $u₂$ individually. That is, \[ \mathcal{V}(\alpha, \gamma, \mathfrak{S}, u₁ \sqcap u₂) = \mathcal{V}(\alpha, \gamma, \mathfrak{S}, u₁) \sqcap \mathcal{V}(\alpha, \gamma, \mathfrak{S}, u₂). \]

UniformOnFun.comap_eq theorem

{f : γ → β} : 𝒱(α, γ, 𝔖, ‹UniformSpace β›.comap f) = 𝒱(α, β, 𝔖, _).comap (f ∘ ·)

Full source

/-- If `u` is a uniform structure on `β` and `f : γ → β`, then
`𝒱(α, γ, 𝔖, comap f u) = comap (fun g ↦ f ∘ g) 𝒱(α, γ, 𝔖, u₁)`. -/
protected theorem comap_eq {f : γ → β} :
    𝒱(α, γ, 𝔖, ‹UniformSpace β›.comap f) = 𝒱(α, β, 𝔖, _).comap (f ∘ ·) := by
  -- We reduce this to `UniformFun.comap_eq` using the fact that `comap` distributes
  -- on `iInf`.
  simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, UniformFun.comap_eq, ←
    UniformSpace.comap_comap]
  -- By definition, `∀ S ∈ 𝔖, (f ∘ —) ∘ S.restrict = S.restrict ∘ (f ∘ —)`.
  rfl

Uniform structure of $\mathfrak{S}$-convergence commutes with pullback via composition

Informal description

Let $\beta$ be a uniform space and $f : \gamma \to \beta$ be a function. Then the uniform structure of $\mathfrak{S}$-convergence on $\alpha \to \gamma$ induced by the pullback uniform structure on $\gamma$ (via $f$) is equal to the pullback of the uniform structure of $\mathfrak{S}$-convergence on $\alpha \to \beta$ under the post-composition map $g \mapsto f \circ g$. That is, \[ \mathcal{V}(\alpha, \gamma, \mathfrak{S}, f^*\mathcal{U}_\beta) = (f \circ \cdot)^* \mathcal{V}(\alpha, \beta, \mathfrak{S}, \mathcal{U}_\beta). \]

UniformOnFun.postcomp_uniformContinuous theorem

 [UniformSpace γ] {f : γ → β} (hf : UniformContinuous f) : UniformContinuous (ofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖)

Full source

/-- Post-composition by a uniformly continuous function is uniformly continuous for the
uniform structures of `𝔖`-convergence.

More precisely, if `f : γ → β` is uniformly continuous, then
`(fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β)` is uniformly continuous. -/
protected theorem postcomp_uniformContinuous [UniformSpace γ] {f : γ → β}
    (hf : UniformContinuous f) : UniformContinuous (ofFunofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖) := by
  -- This is a direct consequence of `UniformOnFun.comap_eq`
  rw [uniformContinuous_iff]
  exact (UniformOnFun.mono (uniformContinuous_iff.mp hf) subset_rfl).trans_eq UniformOnFun.comap_eq

Uniform Continuity of Post-Composition in $\mathfrak{S}$-Convergence

Informal description

Let $\gamma$ and $\beta$ be uniform spaces, and let $f : \gamma \to \beta$ be a uniformly continuous function. Then the post-composition map $g \mapsto f \circ g$ is uniformly continuous from the space $\alpha \to_{\mathfrak{S}} \gamma$ (equipped with the uniform structure of $\mathfrak{S}$-convergence) to the space $\alpha \to_{\mathfrak{S}} \beta$.

UniformOnFun.postcomp_isUniformInducing theorem

 [UniformSpace γ] {f : γ → β} (hf : IsUniformInducing f) : IsUniformInducing (ofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖)

Full source

/-- Post-composition by a uniform inducing is a uniform inducing for the
uniform structures of `𝔖`-convergence.

More precisely, if `f : γ → β` is a uniform inducing, then
`(fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β)` is a uniform inducing. -/
lemma postcomp_isUniformInducing [UniformSpace γ] {f : γ → β}
    (hf : IsUniformInducing f) : IsUniformInducing (ofFunofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖) := by
  -- This is a direct consequence of `UniformOnFun.comap_eq`
  constructor
  replace hf : (𝓤 β).comap (Prod.map f f) = _ := hf.comap_uniformity
  change comap (Prod.map (ofFunofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖) (ofFunofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖)) _ = _
  rw [← uniformity_comap] at hf ⊢
  congr
  rw [← UniformSpace.ext hf, UniformOnFun.comap_eq]
  rfl

Post-composition by a uniform inducing map is uniform inducing for $\mathfrak{S}$-convergence

Informal description

Let $\gamma$ and $\beta$ be uniform spaces, and let $f : \gamma \to \beta$ be a uniform inducing map. Then the post-composition map $(g \mapsto f \circ g) : (\alpha \to_{\mathfrak{S}} \gamma) \to (\alpha \to_{\mathfrak{S}} \beta)$ is also a uniform inducing map, where $\alpha \to_{\mathfrak{S}} \gamma$ and $\alpha \to_{\mathfrak{S}} \beta$ are equipped with the uniform structures of $\mathfrak{S}$-convergence for a family $\mathfrak{S}$ of subsets of $\alpha$.

UniformOnFun.postcomp_isUniformEmbedding theorem

 [UniformSpace γ] {f : γ → β} (hf : IsUniformEmbedding f) : IsUniformEmbedding (ofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖)

Full source

/-- Post-composition by a uniform embedding is a uniform embedding for the
uniform structures of `𝔖`-convergence.

More precisely, if `f : γ → β` is a uniform embedding, then
`(fun g ↦ f ∘ g) : (α →ᵤ[𝔖] γ) → (α →ᵤ[𝔖] β)` is a uniform embedding. -/
protected theorem postcomp_isUniformEmbedding [UniformSpace γ] {f : γ → β}
    (hf : IsUniformEmbedding f) : IsUniformEmbedding (ofFunofFun 𝔖 ∘ (f ∘ ·) ∘ toFun 𝔖) where
  toIsUniformInducing := UniformOnFun.postcomp_isUniformInducing hf.isUniformInducing
  injective _ _ H := funext fun _ ↦ hf.injective (congrFun H _)

Post-composition by a uniform embedding is a uniform embedding for $\mathfrak{S}$-convergence

Informal description

Let $\gamma$ and $\beta$ be uniform spaces, and let $f : \gamma \to \beta$ be a uniform embedding. Then the post-composition map $(g \mapsto f \circ g) : (\alpha \to_{\mathfrak{S}} \gamma) \to (\alpha \to_{\mathfrak{S}} \beta)$ is also a uniform embedding, where $\alpha \to_{\mathfrak{S}} \gamma$ and $\alpha \to_{\mathfrak{S}} \beta$ are equipped with the uniform structures of $\mathfrak{S}$-convergence for a family $\mathfrak{S}$ of subsets of $\alpha$.

UniformOnFun.congrRight definition

[UniformSpace γ] (e : γ ≃ᵤ β) : (α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β)

Full source

/-- Turn a uniform isomorphism `γ ≃ᵤ β` into a uniform isomorphism `(α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β)`
by post-composing. -/
protected def congrRight [UniformSpace γ] (e : γ ≃ᵤ β) : (α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β) :=
  { Equiv.piCongrRight fun _a => e.toEquiv with
    uniformContinuous_toFun := UniformOnFun.postcomp_uniformContinuous e.uniformContinuous
    uniformContinuous_invFun := UniformOnFun.postcomp_uniformContinuous e.symm.uniformContinuous }

Uniform isomorphism of function spaces induced by post-composition with a uniform isomorphism

Informal description

Given a uniform isomorphism $ e : \gamma \simeq_{\mathfrak{u}} \beta $ between uniform spaces, the post-composition map $ (f \mapsto e \circ f) $ induces a uniform isomorphism between the function spaces $ \alpha \to_{\mathfrak{S}} \gamma $ and $ \alpha \to_{\mathfrak{S}} \beta $, both equipped with the uniform structure of $\mathfrak{S}$-convergence.

UniformOnFun.precomp_uniformContinuous theorem

 {𝔗 : Set (Set γ)} {f : γ → α} (hf : MapsTo (f '' ·) 𝔗 𝔖) :
  UniformContinuous fun g : α →ᵤ[𝔖] β => ofFun 𝔗 (toFun 𝔖 g ∘ f)

Full source

/-- Let `f : γ → α`, `𝔖 : Set (Set α)`, `𝔗 : Set (Set γ)`, and assume that `∀ T ∈ 𝔗, f '' T ∈ 𝔖`.
Then, the function `(fun g ↦ g ∘ f) : (α →ᵤ[𝔖] β) → (γ →ᵤ[𝔗] β)` is uniformly continuous.

Note that one can easily see that assuming `∀ T ∈ 𝔗, ∃ S ∈ 𝔖, f '' T ⊆ S` would work too, but
we will get this for free when we prove that `𝒱(α, β, 𝔖, uβ) = 𝒱(α, β, 𝔖', uβ)` where `𝔖'` is the
***noncovering*** bornology generated by `𝔖`. -/
protected theorem precomp_uniformContinuous {𝔗 : Set (Set γ)} {f : γ → α}
    (hf : MapsTo (f '' ·) 𝔗 𝔖) :
    UniformContinuous fun g : α →ᵤ[𝔖] β => ofFun 𝔗 (toFuntoFun 𝔖 g ∘ f) := by
  -- This follows from the fact that `(· ∘ f) × (· ∘ f)` maps `gen (f '' t) V` to `gen t V`.
  simp_rw [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf]
  refine fun t ht V hV ↦ tendsto_iInf' (f '' t) <| tendsto_iInf' (hf ht) <|
    tendsto_iInf' V <| tendsto_iInf' hV ?_
  simpa only [tendsto_principal_principal, UniformOnFun.gen] using fun _ ↦ forall_mem_image.1

Uniform Continuity of Precomposition in Function Spaces with Uniform Convergence

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types, and let $\mathfrak{S}$ be a family of subsets of $\alpha$ and $\mathfrak{T}$ a family of subsets of $\gamma$. Given a function $f : \gamma \to \alpha$ such that for every $T \in \mathfrak{T}$, the image $f(T)$ belongs to $\mathfrak{S}$, then the precomposition map $(g \mapsto g \circ f) : (\alpha \to_{\mathfrak{S}} \beta) \to (\gamma \to_{\mathfrak{T}} \beta)$ is uniformly continuous.

UniformOnFun.congrLeft definition

 {𝔗 : Set (Set γ)} (e : γ ≃ α) (he : 𝔗 ⊆ image e ⁻¹' 𝔖) (he' : 𝔖 ⊆ preimage e ⁻¹' 𝔗) : (γ →ᵤ[𝔗] β) ≃ᵤ (α →ᵤ[𝔖] β)

Full source

/-- Turn a bijection `e : γ ≃ α` such that we have both `∀ T ∈ 𝔗, e '' T ∈ 𝔖` and
`∀ S ∈ 𝔖, e ⁻¹' S ∈ 𝔗` into a uniform isomorphism `(γ →ᵤ[𝔗] β) ≃ᵤ (α →ᵤ[𝔖] β)` by pre-composing. -/
protected def congrLeft {𝔗 : Set (Set γ)} (e : γ ≃ α) (he : 𝔗 ⊆ image e ⁻¹' 𝔖)
    (he' : 𝔖 ⊆ preimage e ⁻¹' 𝔗) : (γ →ᵤ[𝔗] β) ≃ᵤ (α →ᵤ[𝔖] β) :=
  { Equiv.arrowCongr e (Equiv.refl _) with
    uniformContinuous_toFun := UniformOnFun.precomp_uniformContinuous fun s hs ↦ by
      change e.symm '' se.symm '' s ∈ 𝔗
      rw [← preimage_equiv_eq_image_symm]
      exact he' hs
    uniformContinuous_invFun := UniformOnFun.precomp_uniformContinuous he }

Uniform isomorphism of function spaces via domain bijection

Informal description

Given a bijection $e : \gamma \leftrightarrow \alpha$ between types $\gamma$ and $\alpha$, and families of subsets $\mathfrak{T}$ of $\gamma$ and $\mathfrak{S}$ of $\alpha$ satisfying: 1. For every $T \in \mathfrak{T}$, the image $e(T)$ belongs to $\mathfrak{S}$ 2. For every $S \in \mathfrak{S}$, the preimage $e^{-1}(S)$ belongs to $\mathfrak{T}$ Then there exists a uniform isomorphism between the function spaces $\gamma \to_{\mathfrak{T}} \beta$ and $\alpha \to_{\mathfrak{S}} \beta$, induced by precomposition with $e$.

UniformOnFun.t2Space_of_covering theorem

[T2Space β] (h : ⋃₀ 𝔖 = univ) : T2Space (α →ᵤ[𝔖] β)

Full source

/-- If `𝔖` covers `α`, then the topology of `𝔖`-convergence is T₂. -/
theorem t2Space_of_covering [T2Space β] (h : ⋃₀ 𝔖 = univ) : T2Space (α →ᵤ[𝔖] β) where
  t2 f g hfg := by
    obtain ⟨x, hx⟩ := not_forall.mp (mt funext hfg)
    obtain ⟨s, hs, hxs⟩ : ∃ s ∈ 𝔖, x ∈ s := mem_sUnion.mp (h.symm ▸ True.intro)
    exact separated_by_continuous (uniformContinuous_eval_of_mem β 𝔖 hxs hs).continuous hx

Hausdorff Property of $\mathfrak{S}$-Convergence Function Space

Informal description

Let $\beta$ be a Hausdorff topological space and $\mathfrak{S}$ be a family of subsets of $\alpha$ whose union covers $\alpha$ (i.e., $\bigcup_{S \in \mathfrak{S}} S = \alpha$). Then the space of functions $\alpha \to_{\mathfrak{S}} \beta$, equipped with the topology of uniform convergence on $\mathfrak{S}$, is also Hausdorff.

UniformOnFun.uniformContinuous_restrict_toFun theorem

: UniformContinuous ((⋃₀ 𝔖).restrict ∘ toFun 𝔖 : (α →ᵤ[𝔖] β) → ⋃₀ 𝔖 → β)

Full source

/-- The restriction map from `α →ᵤ[𝔖] β` to `⋃₀ 𝔖 → β` is uniformly continuous. -/
theorem uniformContinuous_restrict_toFun :
    UniformContinuous ((⋃₀ 𝔖).restrict ∘ toFun 𝔖 : (α →ᵤ[𝔖] β) → ⋃₀ 𝔖 → β) := by
  rw [uniformContinuous_pi]
  intro ⟨x, hx⟩
  obtain ⟨s : Set α, hs : s ∈ 𝔖, hxs : x ∈ s⟩ := mem_sUnion.mpr hx
  exact uniformContinuous_eval_of_mem β 𝔖 hxs hs

Uniform Continuity of Restriction to Union of $\mathfrak{S}$ in $\mathfrak{S}$-Convergence

Informal description

The restriction map from the space of functions $\alpha \to_{\mathfrak{S}} \beta$ (equipped with the uniform structure of $\mathfrak{S}$-convergence) to the space of functions $\bigcup_{S \in \mathfrak{S}} S \to \beta$ is uniformly continuous. Here, $\mathfrak{S}$ is a family of subsets of $\alpha$.

UniformOnFun.uniformContinuous_toFun theorem

(h : ⋃₀ 𝔖 = univ) : UniformContinuous (toFun 𝔖 : (α →ᵤ[𝔖] β) → α → β)

Full source

/-- If `𝔖` covers `α`, the natural map `UniformOnFun.toFun` from `α →ᵤ[𝔖] β` to `α → β` is
uniformly continuous.

In other words, if `𝔖` covers `α`, then the uniform structure of `𝔖`-convergence is finer than
that of pointwise convergence. -/
protected theorem uniformContinuous_toFun (h : ⋃₀ 𝔖 = univ) :
    UniformContinuous (toFun 𝔖 : (α →ᵤ[𝔖] β) → α → β) := by
  rw [uniformContinuous_pi]
  exact uniformContinuous_eval h

Uniform Continuity of the Natural Map from $\mathfrak{S}$-Convergence to Pointwise Convergence

Informal description

If the union of the family $\mathfrak{S}$ of subsets of $\alpha$ covers $\alpha$ (i.e., $\bigcup_{S \in \mathfrak{S}} S = \alpha$), then the natural map from the space of functions $\alpha \to_{\mathfrak{S}} \beta$ (equipped with the uniform structure of $\mathfrak{S}$-convergence) to the space of all functions $\alpha \to \beta$ is uniformly continuous.

UniformOnFun.continuousAt_eval₂ theorem

 [TopologicalSpace α] {f : α →ᵤ[𝔖] β} {x : α} (h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x) (hc : ContinuousAt (toFun 𝔖 f) x) :
  ContinuousAt (fun fx : (α →ᵤ[𝔖] β) × α ↦ toFun 𝔖 fx.1 fx.2) (f, x)

Full source

/-- If `f : α →ᵤ[𝔖] β` is continuous at `x` and `x` admits a neighbourhood `V ∈ 𝔖`,
then evaluation of `g : α →ᵤ[𝔖] β` at `y : α` is continuous in `(g, y)` at `(f, x)`. -/
protected theorem continuousAt_eval₂ [TopologicalSpace α] {f : α →ᵤ[𝔖] β} {x : α}
    (h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x) (hc : ContinuousAt (toFun 𝔖 f) x) :
    ContinuousAt (fun fx : (α →ᵤ[𝔖] β) × α ↦ toFun 𝔖 fx.1 fx.2) (f, x) := by
  rw [ContinuousAt, nhds_eq_comap_uniformity, tendsto_comap_iff, ← lift'_comp_uniformity,
    tendsto_lift']
  intro U hU
  rcases h𝔖 with ⟨V, hV, hVx⟩
  filter_upwards [prod_mem_nhds (UniformOnFun.gen_mem_nhds _ _ _ hV hU)
    (inter_mem hVx <| hc <| UniformSpace.ball_mem_nhds _ hU)]
    with ⟨g, y⟩ ⟨hg, hyV, hy⟩ using ⟨toFun 𝔖 f y, hy, hg y hyV⟩

Continuity of Evaluation at a Point with Neighborhood in $\mathfrak{S}$

Informal description

Let $\alpha$ and $\beta$ be topological spaces, and let $\mathfrak{S}$ be a family of subsets of $\alpha$. Given a function $f \in \alpha \to_{\mathfrak{S}} \beta$ that is continuous at $x \in \alpha$, and a neighborhood $V \in \mathfrak{S}$ of $x$, the evaluation map $(g, y) \mapsto g(y)$ is continuous at $(f, x)$ in the product space $(\alpha \to_{\mathfrak{S}} \beta) \times \alpha$.

UniformOnFun.continuousOn_eval₂ theorem

 [TopologicalSpace α] (h𝔖 : ∀ x, ∃ V ∈ 𝔖, V ∈ 𝓝 x) :
  ContinuousOn (fun fx : (α →ᵤ[𝔖] β) × α ↦ toFun 𝔖 fx.1 fx.2) {fx | ContinuousAt (toFun 𝔖 fx.1) fx.2}

Full source

/-- If each point of `α` admits a neighbourhood `V ∈ 𝔖`,
then the evaluation of `f : α →ᵤ[𝔖] β` at `x : α` is continuous in `(f, x)`
on the set of `(f, x)` such that `f` is continuous at `x`. -/
protected theorem continuousOn_eval₂ [TopologicalSpace α] (h𝔖 : ∀ x, ∃ V ∈ 𝔖, V ∈ 𝓝 x) :
    ContinuousOn (fun fx : (α →ᵤ[𝔖] β) × α ↦ toFun 𝔖 fx.1 fx.2)
      {fx | ContinuousAt (toFun 𝔖 fx.1) fx.2} := fun (_f, x) hc ↦
  (UniformOnFun.continuousAt_eval₂ (h𝔖 x) hc).continuousWithinAt

Joint Continuity of Evaluation for $\mathfrak{S}$-Convergence on Continuity Points

Informal description

Let $\alpha$ and $\beta$ be topological spaces, and let $\mathfrak{S}$ be a family of subsets of $\alpha$ such that every point $x \in \alpha$ has a neighborhood $V \in \mathfrak{S}$ in its neighborhood filter. Then the evaluation map $(f, x) \mapsto f(x)$ is continuous on the set of pairs $(f, x) \in (\alpha \to_{\mathfrak{S}} \beta) \times \alpha$ where $f$ is continuous at $x$.

UniformOnFun.tendsto_iff_tendstoUniformlyOn theorem

 {F : ι → α →ᵤ[𝔖] β} {f : α →ᵤ[𝔖] β} : Tendsto F p (𝓝 f) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (toFun 𝔖 ∘ F) (toFun 𝔖 f) p s

Full source

/-- Convergence in the topology of `𝔖`-convergence means uniform convergence on `S` (in the sense
of `TendstoUniformlyOn`) for all `S ∈ 𝔖`. -/
protected theorem tendsto_iff_tendstoUniformlyOn {F : ι → α →ᵤ[𝔖] β} {f : α →ᵤ[𝔖] β} :
    TendstoTendsto F p (𝓝 f) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (toFun 𝔖 ∘ F) (toFun 𝔖 f) p s := by
  simp only [UniformOnFun.nhds_eq, tendsto_iInf, tendsto_principal, TendstoUniformlyOn,
    Function.comp_apply, mem_setOf]

Characterization of Convergence in $\mathfrak{S}$-Convergence Topology via Uniform Convergence on Each Set in $\mathfrak{S}$

Informal description

Let $\mathfrak{S}$ be a family of subsets of $\alpha$, and let $F : \iota \to \alpha \to_{\mathfrak{S}} \beta$ be a net of functions and $f : \alpha \to_{\mathfrak{S}} \beta$ be a function. Then $F$ converges to $f$ in the topology of $\mathfrak{S}$-convergence if and only if for every $s \in \mathfrak{S}$, the net $(F_i)$ converges uniformly to $f$ on $s$.

UniformOnFun.continuous_rng_iff theorem

 {X : Type*} [TopologicalSpace X] {f : X → (α →ᵤ[𝔖] β)} :
  Continuous f ↔ ∀ s ∈ 𝔖, Continuous (UniformFun.ofFun ∘ s.restrict ∘ UniformOnFun.toFun 𝔖 ∘ f)

Full source

protected lemma continuous_rng_iff {X : Type*} [TopologicalSpace X] {f : X → (α →ᵤ[𝔖] β)} :
    ContinuousContinuous f ↔ ∀ s ∈ 𝔖,
      Continuous (UniformFun.ofFun ∘ s.restrict ∘ UniformOnFun.toFun 𝔖 ∘ f) := by
  simp only [continuous_iff_continuousAt, ContinuousAt,
    UniformOnFun.tendsto_iff_tendstoUniformlyOn, UniformFun.tendsto_iff_tendstoUniformly,
    tendstoUniformlyOn_iff_tendstoUniformly_comp_coe, @forall_swap X, Function.comp_apply,
    Function.comp_def, restrict_eq, UniformFun.toFun_ofFun]

Characterization of Continuity for $\mathfrak{S}$-Convergence Function Spaces

Informal description

Let $X$ be a topological space and $f : X \to \alpha \to_{\mathfrak{S}} \beta$ be a function. Then $f$ is continuous if and only if for every set $s$ in the family $\mathfrak{S}$ of subsets of $\alpha$, the composition $\text{UniformFun.ofFun} \circ s.\text{restrict} \circ \text{UniformOnFun.toFun} \circ f$ is continuous, where: - $\text{UniformOnFun.toFun}$ converts from $\alpha \to_{\mathfrak{S}} \beta$ to $\alpha \to \beta$, - $s.\text{restrict}$ restricts a function $\alpha \to \beta$ to $s \to \beta$, - $\text{UniformFun.ofFun}$ converts back to the uniform convergence space $s \toᵤ \beta$.

UniformOnFun.instCompleteSpace instance

[CompleteSpace β] : CompleteSpace (α →ᵤ[𝔖] β)

Full source

instance [CompleteSpace β] : CompleteSpace (α →ᵤ[𝔖] β) := by
  rcases isEmpty_or_nonempty β
  · infer_instance
  · refine ⟨fun {F} hF ↦ ?_⟩
    have := hF.1
    have : ∀ x ∈ ⋃₀ 𝔖, ∃ y : β, Tendsto (toFun 𝔖 · x) F (𝓝 y) := fun x hx ↦
      CompleteSpace.complete (hF.map (uniformContinuous_eval_of_mem_sUnion _ _ hx))
    choose! g hg using this
    use ofFun 𝔖 g
    simp_rw [UniformOnFun.nhds_eq_of_basis _ _ uniformity_hasBasis_closed, le_iInf₂_iff,
      le_principal_iff]
    intro s hs U ⟨hU, hUc⟩
    rcases cauchy_iff.mp hF |>.2 _ <| UniformOnFun.gen_mem_uniformity _ _ hs hU
      with ⟨V, hV, hVU⟩
    filter_upwards [hV] with f hf x hx
    refine hUc.mem_of_tendsto ((hg x ⟨s, hs, hx⟩).prodMk_nhds tendsto_const_nhds) ?_
    filter_upwards [hV] with g' hg' using hVU (mk_mem_prod hg' hf) _ hx

Completeness of Function Space with Uniform Convergence on a Family of Sets

Informal description

For any uniform space $\beta$ that is complete, the space of functions $\alpha \to_{\mathfrak{S}} \beta$ equipped with the uniform structure of $\mathfrak{S}$-convergence is also complete. Here $\mathfrak{S}$ is a family of subsets of $\alpha$.

UniformOnFun.uniformEquivProdArrow definition

[UniformSpace γ] : (α →ᵤ[𝔖] β × γ) ≃ᵤ (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)

Full source

/-- The natural bijection between `α → β × γ` and `(α → β) × (α → γ)`, upgraded to a uniform
isomorphism between `α →ᵤ[𝔖] β × γ` and `(α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)`. -/
protected def uniformEquivProdArrow [UniformSpace γ] :
    (α →ᵤ[𝔖] β × γ) ≃ᵤ (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ) :=
  -- Denote `φ` this bijection. We want to show that
  -- `comap φ (𝒱(α, β, 𝔖, uβ) × 𝒱(α, γ, 𝔖, uγ)) = 𝒱(α, β × γ, 𝔖, uβ × uγ)`.
  -- But `uβ × uγ` is defined as `comap fst uβ ⊓ comap snd uγ`, so we just have to apply
  -- `UniformOnFun.inf_eq` and `UniformOnFun.comap_eq`,
  -- which leaves us to check that some square commutes.
  -- We could also deduce this from `UniformFun.uniformEquivProdArrow`,
  -- but it turns out to be more annoying.
  ((UniformOnFun.ofFun 𝔖).symm.trans <| (Equiv.arrowProdEquivProdArrow _ _ _).trans <|
    (UniformOnFun.ofFun 𝔖).prodCongr (UniformOnFun.ofFun 𝔖)).toUniformEquivOfIsUniformInducing <| by
      constructor
      rw [uniformity_prod, comap_inf, comap_comap, comap_comap]
      have H := @UniformOnFun.inf_eq α (β × γ) 𝔖
        (UniformSpace.comap Prod.fst ‹_›) (UniformSpace.comap Prod.snd ‹_›)
      apply_fun (fun u ↦ @uniformity (α →ᵤ[𝔖] β × γ) u) at H
      convert H.symm using 1
      rw [UniformOnFun.comap_eq, UniformOnFun.comap_eq]
      erw [inf_uniformity]
      rw [uniformity_comap, uniformity_comap]
      rfl

Uniform isomorphism between product-valued functions and pairs of functions under $\mathfrak{S}$-convergence

Informal description

The natural bijection between the space of functions $\alpha \to_{\mathfrak{S}} (\beta \times \gamma)$ and the product space $(\alpha \to_{\mathfrak{S}} \beta) \times (\alpha \to_{\mathfrak{S}} \gamma)$, upgraded to a uniform isomorphism. Here, $\alpha \to_{\mathfrak{S}} \beta$ denotes the space of functions from $\alpha$ to $\beta$ equipped with the uniform structure of uniform convergence on a family $\mathfrak{S}$ of subsets of $\alpha$.

UniformOnFun.uniformEquivPiComm definition

: (α →ᵤ[𝔖] ((i : ι) → δ i)) ≃ᵤ ((i : ι) → α →ᵤ[𝔖] δ i)

Full source

/-- The natural bijection between `α → Π i, δ i` and `Π i, α → δ i`, upgraded to a uniform
isomorphism between `α →ᵤ[𝔖] (Π i, δ i)` and `Π i, α →ᵤ[𝔖] δ i`. -/
protected def uniformEquivPiComm : (α →ᵤ[𝔖] ((i : ι) → δ i)) ≃ᵤ ((i : ι) → α →ᵤ[𝔖] δ i) :=
  -- Denote `φ` this bijection. We want to show that
  -- `comap φ (Π i, 𝒱(α, δ i, 𝔖, uδ i)) = 𝒱(α, (Π i, δ i), 𝔖, (Π i, uδ i))`.
  -- But `Π i, uδ i` is defined as `⨅ i, comap (eval i) (uδ i)`, so we just have to apply
  -- `UniformOnFun.iInf_eq` and `UniformOnFun.comap_eq`,
  -- which leaves us to check that some square commutes.
  -- We could also deduce this from `UniformFun.uniformEquivPiComm`, but it turns out
  -- to be more annoying.
  @Equiv.toUniformEquivOfIsUniformInducing (α →ᵤ[𝔖] ((i : ι) → δ i)) ((i : ι) → α →ᵤ[𝔖] δ i)
      _ _ (Equiv.piComm _) <| by
    constructor
    change comap (Prod.map Function.swap Function.swap) _ = _
    erw [← uniformity_comap]
    congr
    rw [Pi.uniformSpace, UniformSpace.ofCoreEq_toCore, Pi.uniformSpace,
      UniformSpace.ofCoreEq_toCore, UniformSpace.comap_iInf, UniformOnFun.iInf_eq]
    refine iInf_congr fun i => ?_
    rw [← UniformSpace.comap_comap, UniformOnFun.comap_eq]
    rfl

Uniform isomorphism between function space and product space under $\mathfrak{S}$-convergence

Informal description

The natural bijection between the space of functions $\alpha \to_{\mathfrak{S}} (\Pi_{i \in \iota} \delta_i)$ (equipped with the uniform structure of $\mathfrak{S}$-convergence) and the product space $\Pi_{i \in \iota} (\alpha \to_{\mathfrak{S}} \delta_i)$ is a uniform isomorphism. Here $\mathfrak{S}$ is a family of subsets of $\alpha$, and each $\delta_i$ is a uniform space.

UniformOnFun.isClosed_setOf_continuous theorem

[TopologicalSpace α] (h : IsCoherentWith 𝔖) : IsClosed {f : α →ᵤ[𝔖] β | Continuous (toFun 𝔖 f)}

Full source

/-- Suppose that the topology on `α` is defined by its restrictions to the sets of `𝔖`.

Then the set of continuous functions is closed
in the topology of uniform convergence on the sets of `𝔖`. -/
theorem isClosed_setOf_continuous [TopologicalSpace α] (h : IsCoherentWith 𝔖) :
    IsClosed {f : α →ᵤ[𝔖] β | Continuous (toFun 𝔖 f)} := by
  refine isClosed_iff_forall_filter.2 fun f u _ hu huf ↦ h.continuous_iff.2 fun s hs ↦ ?_
  rw [← tendsto_id', UniformOnFun.tendsto_iff_tendstoUniformlyOn] at huf
  exact (huf s hs).continuousOn <| hu fun _ ↦ Continuous.continuousOn

Closedness of Continuous Functions in Uniform $\mathfrak{S}$-Convergence Topology

Informal description

Let $\alpha$ be a topological space and $\mathfrak{S}$ be a family of subsets of $\alpha$ such that the topology on $\alpha$ is coherent with $\mathfrak{S}$ (i.e., a set is open in $\alpha$ if and only if its intersection with each $S \in \mathfrak{S}$ is open in $S$). Then the set of continuous functions from $\alpha$ to $\beta$ is closed in the space $\alpha \to_{\mathfrak{S}} \beta$ equipped with the topology of uniform convergence on the sets in $\mathfrak{S}$.

UniformOnFun.uniformSpace_eq_inf_precomp_of_cover theorem

 {δ₁ δ₂ : Type*} (φ₁ : δ₁ → α) (φ₂ : δ₂ → α) (𝔗₁ : Set (Set δ₁)) (𝔗₂ : Set (Set δ₂)) (h_image₁ : MapsTo (φ₁ '' ·) 𝔗₁ 𝔖)
  (h_image₂ : MapsTo (φ₂ '' ·) 𝔗₂ 𝔖) (h_preimage₁ : MapsTo (φ₁ ⁻¹' ·) 𝔖 𝔗₁) (h_preimage₂ : MapsTo (φ₂ ⁻¹' ·) 𝔖 𝔗₂)
  (h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂) :
  𝒱(α, β, 𝔖, _) =
    .comap (ofFun 𝔗₁ ∘ (· ∘ φ₁) ∘ toFun 𝔖) 𝒱(δ₁, β, 𝔗₁, _) ⊓ .comap (ofFun 𝔗₂ ∘ (· ∘ φ₂) ∘ toFun 𝔖) 𝒱(δ₂, β, 𝔗₂, _)

Full source

theorem uniformSpace_eq_inf_precomp_of_cover {δ₁ δ₂ : Type*} (φ₁ : δ₁ → α) (φ₂ : δ₂ → α)
    (𝔗₁ : Set (Set δ₁)) (𝔗₂ : Set (Set δ₂))
    (h_image₁ : MapsTo (φ₁ '' ·) 𝔗₁ 𝔖) (h_image₂ : MapsTo (φ₂ '' ·) 𝔗₂ 𝔖)
    (h_preimage₁ : MapsTo (φ₁ ⁻¹' ·) 𝔖 𝔗₁) (h_preimage₂ : MapsTo (φ₂ ⁻¹' ·) 𝔖 𝔗₂)
    (h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂) :
    𝒱(α, β, 𝔖, _) =
      .comap.comap (ofFun 𝔗₁ ∘ (· ∘ φ₁) ∘ toFun 𝔖) 𝒱(δ₁, β, 𝔗₁, _) ⊓
      .comap (ofFun 𝔗₂ ∘ (· ∘ φ₂) ∘ toFun 𝔖) 𝒱(δ₂, β, 𝔗₂, _) := by
  set ψ₁ : Π S : Set α, φ₁ ⁻¹' S → S := fun S ↦ S.restrictPreimage φ₁
  set ψ₂ : Π S : Set α, φ₂ ⁻¹' S → S := fun S ↦ S.restrictPreimage φ₂
  have : ∀ S ∈ 𝔖, 𝒰(S, β, _) = .comap (· ∘ ψ₁ S) 𝒰(_, β, _) ⊓ .comap (· ∘ ψ₂ S) 𝒰(_, β, _) := by
    refine fun S hS ↦ UniformFun.uniformSpace_eq_inf_precomp_of_cover β _ _ ?_
    simpa only [← univ_subset_iff, ψ₁, ψ₂, range_restrictPreimage, ← preimage_union,
      ← image_subset_iff, image_univ, Subtype.range_val] using h_cover S hS
  refine le_antisymm (le_inf ?_ ?_) (le_iInf₂ fun S hS ↦ ?_)
  · rw [← uniformContinuous_iff]
    exact UniformOnFun.precomp_uniformContinuous h_image₁
  · rw [← uniformContinuous_iff]
    exact UniformOnFun.precomp_uniformContinuous h_image₂
  · #adaptation_note
    /-- 2025-03-29 lean4#7717 a single `simp_rw` needed to be broken up to fully apply -/
    simp_rw [this S hS]
    conv => enter [1]; rw [UniformSpace.comap_iInf]; enter [1,1,i]; rw [UniformSpace.comap_iInf]
    conv => enter [1]; rw [UniformSpace.comap_iInf]; enter [2,1,i]; rw [UniformSpace.comap_iInf]
    simp_rw [UniformSpace.comap_inf, ← UniformSpace.comap_comap]
    exact inf_le_inf
      (iInf₂_le_of_le _ (h_preimage₁ hS) le_rfl)
      (iInf₂_le_of_le _ (h_preimage₂ hS) le_rfl)

Uniform Structure of $\mathfrak{S}$-Convergence as Infimum of Precomposition Pullbacks under Covering Condition

Informal description

Let $\alpha$, $\beta$, $\delta_1$, and $\delta_2$ be types, and let $\mathfrak{S}$ be a family of subsets of $\alpha$. Given functions $\phi_1 \colon \delta_1 \to \alpha$ and $\phi_2 \colon \delta_2 \to \alpha$, and families $\mathfrak{T}_1$ and $\mathfrak{T}_2$ of subsets of $\delta_1$ and $\delta_2$ respectively, such that: 1. For any $T \in \mathfrak{T}_1$, the image $\phi_1(T)$ belongs to $\mathfrak{S}$, 2. For any $T \in \mathfrak{T}_2$, the image $\phi_2(T)$ belongs to $\mathfrak{S}$, 3. For any $S \in \mathfrak{S}$, the preimage $\phi_1^{-1}(S)$ belongs to $\mathfrak{T}_1$, 4. For any $S \in \mathfrak{S}$, the preimage $\phi_2^{-1}(S)$ belongs to $\mathfrak{T}_2$, 5. Every set $S \in \mathfrak{S}$ is contained in the union of the ranges of $\phi_1$ and $\phi_2$, then the uniform structure $\mathcal{V}(\alpha, \beta, \mathfrak{S})$ of $\mathfrak{S}$-convergence on $\alpha \to \beta$ is equal to the infimum of the pullbacks of the uniform structures $\mathcal{V}(\delta_1, \beta, \mathfrak{T}_1)$ and $\mathcal{V}(\delta_2, \beta, \mathfrak{T}_2)$ under the precomposition maps $g \mapsto g \circ \phi_1$ and $g \mapsto g \circ \phi_2$, respectively.

UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover theorem

 {δ : ι → Type*} (φ : Π i, δ i → α) (𝔗 : ∀ i, Set (Set (δ i))) (h_image : ∀ i, MapsTo (φ i '' ·) (𝔗 i) 𝔖)
  (h_preimage : ∀ i, MapsTo (φ i ⁻¹' ·) 𝔖 (𝔗 i)) (h_cover : ∀ S ∈ 𝔖, ∃ I : Set ι, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)) :
  𝒱(α, β, 𝔖, _) = ⨅ i, .comap (ofFun (𝔗 i) ∘ (· ∘ φ i) ∘ toFun 𝔖) 𝒱(δ i, β, 𝔗 i, _)

Full source

theorem uniformSpace_eq_iInf_precomp_of_cover {δ : ι → Type*} (φ : Π i, δ i → α)
    (𝔗 : ∀ i, Set (Set (δ i))) (h_image : ∀ i, MapsTo (φ i '' ·) (𝔗 i) 𝔖)
    (h_preimage : ∀ i, MapsTo (φ i ⁻¹' ·) 𝔖 (𝔗 i))
    (h_cover : ∀ S ∈ 𝔖, ∃ I : Set ι, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)) :
    𝒱(α, β, 𝔖, _) = ⨅ i, .comap (ofFun (𝔗 i) ∘ (· ∘ φ i) ∘ toFun 𝔖) 𝒱(δ i, β, 𝔗 i, _) := by
  set ψ : Π S : Set α, Π i : ι, (φ i) ⁻¹' S → S := fun S i ↦ S.restrictPreimage (φ i)
  have : ∀ S ∈ 𝔖, 𝒰(S, β, _) = ⨅ i, .comap (· ∘ ψ S i) 𝒰(_, β, _) := fun S hS ↦ by
    rcases h_cover S hS with ⟨I, I_finite, I_cover⟩
    refine UniformFun.uniformSpace_eq_iInf_precomp_of_cover β _ ⟨I, I_finite, ?_⟩
    simpa only [← univ_subset_iff, ψ, range_restrictPreimage, ← preimage_iUnion₂,
      ← image_subset_iff, image_univ, Subtype.range_val] using I_cover
  -- With a better theory of ideals we may be able to simplify the following by replacing `𝔗 i`
  -- by `(φ i ⁻¹' ·) '' 𝔖`.
  refine le_antisymm (le_iInf fun i ↦ ?_) (le_iInf₂ fun S hS ↦ ?_)
  · rw [← uniformContinuous_iff]
    exact UniformOnFun.precomp_uniformContinuous (h_image i)
  · simp_rw [this S hS]
    #adaptation_note /-- 2025-03-29 lean4#7717 needed this additional rw for the `simp_rw` -/
    conv => enter [1,1,i]; rw [UniformSpace.comap_iInf]
    simp_rw [UniformSpace.comap_iInf, ← UniformSpace.comap_comap]
    exact iInf_mono fun i ↦ iInf₂_le_of_le _ (h_preimage i hS) le_rfl

Uniform Structure of $\mathfrak{S}$-Convergence as Infimum of Precomposition Structures under Finite Cover Condition

Informal description

Let $\{\delta_i\}_{i \in \iota}$ be a family of types, $\varphi_i : \delta_i \to \alpha$ a family of functions, and $\mathfrak{T}_i$ a family of subsets of $\delta_i$ for each $i \in \iota$. Suppose that for each $i$, the image $\varphi_i(T)$ belongs to $\mathfrak{S}$ for every $T \in \mathfrak{T}_i$, and the preimage $\varphi_i^{-1}(S)$ belongs to $\mathfrak{T}_i$ for every $S \in \mathfrak{S}$. Furthermore, assume that for every $S \in \mathfrak{S}$, there exists a finite subset $I \subseteq \iota$ such that $S$ is covered by the union of the ranges of $\varphi_i$ for $i \in I$. Then the uniform structure of $\mathfrak{S}$-convergence on $\alpha \to \beta$ is equal to the infimum of the uniform structures obtained by precomposing with each $\varphi_i$ and pulling back the uniform structure of $\mathfrak{T}_i$-convergence on $\delta_i \to \beta$.

UniformFun.instCompleteSpace instance

{α β : Type*} [UniformSpace β] [CompleteSpace β] : CompleteSpace (α →ᵤ β)

Full source

instance {α β : Type*} [UniformSpace β] [CompleteSpace β] : CompleteSpace (α →ᵤ β) :=
  (UniformOnFun.uniformEquivUniformFun β {univ} (mem_singleton _)).completeSpace_iff.1 inferInstance

Completeness of Function Space with Uniform Convergence

Informal description

For any uniform space $\beta$ that is complete, the space of functions $\alpha \toᵤ \beta$ equipped with the uniform structure of uniform convergence is also complete.

UniformContinuousOn.comp_tendstoUniformly theorem

 (s : Set β) (F : ι → α → β) (f : α → β) (hF : ∀ i x, F i x ∈ s) (hf : ∀ x, f x ∈ s) {g : β → γ}
  (hg : UniformContinuousOn g s) (h : TendstoUniformly F f p) :
  TendstoUniformly (fun i x => g (F i x)) (fun x => g (f x)) p

Full source

/-- Composing on the left by a uniformly continuous function preserves uniform convergence -/
theorem UniformContinuousOn.comp_tendstoUniformly (s : Set β) (F : ι → α → β) (f : α → β)
    (hF : ∀ i x, F i x ∈ s) (hf : ∀ x, f x ∈ s)
    {g : β → γ} (hg : UniformContinuousOn g s) (h : TendstoUniformly F f p) :
    TendstoUniformly (fun i x => g (F i x)) (fun x => g (f x)) p := by
  rw [uniformContinuousOn_iff_restrict] at hg
  lift F to ι → α → s using hF with F' hF'
  lift f to α → s using hf with f' hf'
  rw [tendstoUniformly_iff_tendsto] at h
  have : Tendsto (fun q : ι × α ↦ (f' q.2, (F' q.1 q.2))) (p ×ˢ ⊤) (𝓤 s) :=
    h.of_tendsto_comp isUniformEmbedding_subtype_val.comap_uniformity.le
  apply UniformContinuous.comp_tendstoUniformly hg ?_
  rwa [← tendstoUniformly_iff_tendsto] at this

Uniform Continuity Preserves Uniform Convergence under Composition

Informal description

Let $s$ be a subset of $\beta$, and let $F : \iota \to \alpha \to \beta$ and $f : \alpha \to \beta$ be functions such that for all $i \in \iota$ and $x \in \alpha$, $F_i(x) \in s$, and for all $x \in \alpha$, $f(x) \in s$. If $g : \beta \to \gamma$ is uniformly continuous on $s$ and $F$ converges uniformly to $f$ with respect to the filter $p$, then the composition $g \circ F$ converges uniformly to $g \circ f$ with respect to $p$.

UniformContinuousOn.comp_tendstoUniformly_eventually theorem

 (s : Set β) (F : ι → α → β) (f : α → β) (hF : ∀ᶠ i in p, ∀ x, F i x ∈ s) (hf : ∀ x, f x ∈ s) {g : β → γ}
  (hg : UniformContinuousOn g s) (h : TendstoUniformly F f p) :
  TendstoUniformly (fun i => fun x => g (F i x)) (fun x => g (f x)) p

Full source

theorem UniformContinuousOn.comp_tendstoUniformly_eventually (s : Set β) (F : ι → α → β) (f : α → β)
    (hF : ∀ᶠ i in p, ∀ x, F i x ∈ s) (hf : ∀ x, f x ∈ s)
    {g : β → γ} (hg : UniformContinuousOn g s) (h : TendstoUniformly F f p) :
    TendstoUniformly (fun i => fun x => g (F i x)) (fun x => g (f x)) p := by
  classical
  rw [eventually_iff_exists_mem] at hF
  obtain ⟨s', hs', hs⟩ := hF
  let F' : ι → α → β := fun (i : ι) x => if i ∈ s' then F i x else f x
  have hF : F =ᶠ[p] F' :=  by
    rw [eventuallyEq_iff_exists_mem]
    refine ⟨s', hs', fun y hy => by aesop⟩
  have h' : TendstoUniformly F' f p := by
    rwa [tendstoUniformly_congr hF] at h
  apply (tendstoUniformly_congr _).mpr
    (UniformContinuousOn.comp_tendstoUniformly s F' f (by aesop) hf hg h')
  rw [eventuallyEq_iff_exists_mem]
  refine ⟨s', hs', fun i hi => by aesop⟩

Uniform Continuity Preserves Uniform Convergence under Composition (Eventual Version)

Informal description

Let $s$ be a subset of $\beta$, and let $F : \iota \to \alpha \to \beta$ and $f : \alpha \to \beta$ be functions such that for all $x \in \alpha$, $f(x) \in s$, and for eventually all $i$ in the filter $p$, $F_i(x) \in s$ for all $x \in \alpha$. If $g : \beta \to \gamma$ is uniformly continuous on $s$ and $F$ converges uniformly to $f$ with respect to the filter $p$, then the composition $g \circ F$ converges uniformly to $g \circ f$ with respect to $p$.