# Topology and uniform structure of uniform convergence #

This file 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 `UniformSpace`s 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

source
def UniformFun (α : Type u_1) (β : Type u_2) :
Type (max u_1 u_2)

The type of functions from `α` to `β` equipped with the uniform structure and topology of uniform convergence. We denote it `α →ᵤ β`.

Equations

- UniformFun α β = (α → β)

Instances For

source
def UniformOnFun (α : Type u_1) (β : Type u_2) :
Set (Set α) → Type (max u_1 u_2)

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 `α →ᵤ[𝔖] β`.

Equations

- UniformOnFun α β x✝ = (α → β)

Instances For

source
def UniformConvergence.«term_→ᵤ_» :
Lean.TrailingParserDescr

The type of functions from `α` to `β` equipped with the uniform structure and topology of uniform convergence. We denote it `α →ᵤ β`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def UniformConvergence.«term_→ᵤ[_]_» :
Lean.TrailingParserDescr

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 `α →ᵤ[𝔖] β`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance instNonemptyUniformFun {α : Type u_1} {β : Type u_2} [Nonempty β] :
Nonempty (UniformFun α β)
source
instance instNonemptyUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Nonempty β] :
Nonempty (UniformOnFun α β 𝔖)
source
instance instSubsingletonUniformFun {α : Type u_1} {β : Type u_2} [Subsingleton β] :
Subsingleton (UniformFun α β)
source
instance instSubsingletonUniformOnFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Subsingleton β] :
Subsingleton (UniformOnFun α β 𝔖)
source
def UniformFun.ofFun {α : Type u_1} {β : Type u_2} :
(α → β) ≃ UniformFun α β

Reinterpret `f : α → β` as an element of `α →ᵤ β`.

Equations

- UniformFun.ofFun = { toFun := fun (x : α → β) => x, invFun := fun (x : UniformFun α β) => x, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
def UniformOnFun.ofFun {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)) :
(α → β) ≃ UniformOnFun α β 𝔖

Reinterpret `f : α → β` as an element of `α →ᵤ[𝔖] β`.

Equations

- UniformOnFun.ofFun 𝔖 = { toFun := fun (x : α → β) => x, invFun := fun (x : UniformOnFun α β 𝔖) => x, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
def UniformFun.toFun {α : Type u_1} {β : Type u_2} :
UniformFun α β ≃ (α → β)

Reinterpret `f : α →ᵤ β` as an element of `α → β`.

Equations

- UniformFun.toFun = UniformFun.ofFun.symm

Instances For

source
def UniformOnFun.toFun {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)) :
UniformOnFun α β 𝔖 ≃ (α → β)

Reinterpret `f : α →ᵤ[𝔖] β` as an element of `α → β`.

Equations

- UniformOnFun.toFun 𝔖 = (UniformOnFun.ofFun 𝔖).symm

Instances For

source
@[simp]
theorem UniformFun.toFun_ofFun {α : Type u_1} {β : Type u_2} (f : α → β) :
toFun (ofFun f) = f
source
@[simp]
theorem UniformFun.ofFun_toFun {α : Type u_1} {β : Type u_2} (f : UniformFun α β) :
ofFun (toFun f) = f
source
@[simp]
theorem UniformOnFun.toFun_ofFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} (f : α → β) :
(toFun 𝔖) ((ofFun 𝔖) f) = f
source
@[simp]
theorem UniformOnFun.ofFun_toFun {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} (f : UniformOnFun α β 𝔖) :
(ofFun 𝔖) ((toFun 𝔖) f) = f
source
def UniformFun.gen (α : Type u_1) (β : Type u_2) (V : Set (β × β)) :
Set (UniformFun α β × UniformFun α β)

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`.

Equations

- UniformFun.gen α β V = {uv : UniformFun α β × UniformFun α β | ∀ (x : α), (UniformFun.toFun uv.1 x, UniformFun.toFun uv.2 x) ∈ V}

Instances For

source
theorem UniformFun.isBasis_gen (α : Type u_1) (β : Type u_2) (𝓑 : Filter (β × β)) :
Filter.IsBasis (fun (V : Set (β × β)) => V ∈ 𝓑) (UniformFun.gen α β)

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`).

source
def UniformFun.basis (α : Type u_1) (β : Type u_2) (𝓕 : Filter (β × β)) :
FilterBasis (UniformFun α β × UniformFun α β)

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`).

Equations

- UniformFun.basis α β 𝓕 = ⋯.filterBasis

Instances For

source
def UniformFun.filter (α : Type u_1) (β : Type u_2) (𝓕 : Filter (β × β)) :
Filter (UniformFun α β × UniformFun α β)

For `𝓕 : Filter (β × β)`, this is the filter generated by the filter basis `UniformFun.basis α β 𝓕`. For `𝓕 = 𝓤 β`, this will be the uniformity of uniform convergence on `α`.

Equations

- UniformFun.filter α β 𝓕 = (UniformFun.basis α β 𝓕).filter

Instances For

source
def UniformFun.phi (α : Type u_5) (β : Type u_6) (uvx : (UniformFun α β × UniformFun α β) × α) :
β × β
Equations

- UniformFun.phi α β uvx = (uvx.1.1 uvx.2, uvx.1.2 uvx.2)

Instances For

source
theorem UniformFun.gc (α : Type u_1) (β : Type u_2) :
GaloisConnection (fun (𝓐 : Filter (UniformFun α β × UniformFun α β)) => Filter.map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun (𝓕 : Filter (β × β)) => UniformFun.filter α β 𝓕

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`).

source
def UniformFun.uniformCore (α : Type u_1) (β : Type u_2) [UniformSpace β] :
UniformSpace.Core (UniformFun α β)

Core of the uniform structure of uniform convergence.

Equations

- UniformFun.uniformCore α β = UniformSpace.Core.mkOfBasis (UniformFun.basis α β (uniformity β)) ⋯ ⋯ ⋯

Instances For

source
instance UniformFun.uniformSpace (α : Type u_1) (β : Type u_2) [UniformSpace β] :
UniformSpace (UniformFun α β)

Uniform structure of uniform convergence, declared as an instance on `α →ᵤ β`. We will denote it `𝒰(α, β, uβ)` in the rest of this file.

Equations

- UniformFun.uniformSpace α β = UniformSpace.ofCore (UniformFun.uniformCore α β)

source
instance UniformFun.topologicalSpace (α : Type u_1) (β : Type u_2) [UniformSpace β] :
TopologicalSpace (UniformFun α β)

Topology of uniform convergence, declared as an instance on `α →ᵤ β`.

Equations

- UniformFun.topologicalSpace α β = inferInstance

source
theorem UniformFun.hasBasis_uniformity (α : Type u_1) (β : Type u_2) [UniformSpace β] :
(uniformity (UniformFun α β)).HasBasis (fun (x : Set (β × β)) => x ∈ uniformity β) (UniformFun.gen α β)

By definition, the uniformity of `α →ᵤ β` admits the family `{(f, g) | ∀ x, (f x, g x) ∈ V}` for `V ∈ 𝓤 β` as a filter basis.

source
theorem UniformFun.hasBasis_uniformity_of_basis (α : Type u_1) (β : Type u_2) [UniformSpace β] {ι : Sort u_5} {p : ι → Prop} {s : ι → Set (β × β)} (h : (uniformity β).HasBasis p s) :
(uniformity (UniformFun α β)).HasBasis p (UniformFun.gen α β ∘ s)

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).

source
theorem UniformFun.hasBasis_nhds_of_basis (α : Type u_1) (β : Type u_2) {ι : Type u_4} [UniformSpace β] (f : UniformFun α β) {p : ι → Prop} {s : ι → Set (β × β)} (h : (uniformity β).HasBasis p s) :
(nhds f).HasBasis p fun (i : ι) => {g : UniformFun α β | (f, g) ∈ UniformFun.gen α β (s i)}

For `f : α →ᵤ β`, `𝓝 f` admits the family `{g | ∀ x, (f x, g x) ∈ V}` for `V ∈ 𝓑` as a filter basis, for any basis `𝓑` of `𝓤 β`.

source
theorem UniformFun.hasBasis_nhds (α : Type u_1) (β : Type u_2) [UniformSpace β] (f : UniformFun α β) :
(nhds f).HasBasis (fun (V : Set (β × β)) => V ∈ uniformity β) fun (V : Set (β × β)) => {g : UniformFun α β | (f, g) ∈ UniformFun.gen α β V}

For `f : α →ᵤ β`, `𝓝 f` admits the family `{g | ∀ x, (f x, g x) ∈ V}` for `V ∈ 𝓤 β` as a filter basis.

source
theorem UniformFun.uniformContinuous_eval {α : Type u_1} (β : Type u_2) [UniformSpace β] (x : α) :
UniformContinuous (Function.eval x ∘ ⇑toFun)

Evaluation at a fixed point is uniformly continuous on `α →ᵤ β`.

source
@[simp]
theorem UniformFun.mem_gen {α : Type u_1} {β : Type u_5} {f g : UniformFun α β} {V : Set (β × β)} :
(f, g) ∈ UniformFun.gen α β V ↔ ∀ (x : α), (toFun f x, toFun g x) ∈ V
source
theorem UniformFun.mono {α : Type u_1} {γ : Type u_3} :
Monotone (@uniformSpace α γ)

If `u₁` and `u₂` are two uniform structures on `γ` and `u₁ ≤ u₂`, then `𝒰(α, γ, u₁) ≤ 𝒰(α, γ, u₂)`.

source
theorem UniformFun.iInf_eq {α : Type u_1} {γ : Type u_3} {ι : Type u_4} {u : ι → UniformSpace γ} :
uniformSpace α γ = ⨅ (i : ι), uniformSpace α γ

If `u` is a family of uniform structures on `γ`, then `𝒰(α, γ, (⨅ i, u i)) = ⨅ i, 𝒰(α, γ, u i)`.

source
theorem UniformFun.inf_eq {α : Type u_1} {γ : Type u_3} {u₁ u₂ : UniformSpace γ} :
uniformSpace α γ = uniformSpace α γ ⊓ uniformSpace α γ

If `u₁` and `u₂` are two uniform structures on `γ`, then `𝒰(α, γ, u₁ ⊓ u₂) = 𝒰(α, γ, u₁) ⊓ 𝒰(α, γ, u₂)`.

source
theorem UniformFun.postcomp_isUniformInducing {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] [UniformSpace γ] {f : γ → β} (hf : IsUniformInducing f) :
IsUniformInducing (⇑ofFun ∘ (fun (x : α → γ) => f ∘ x) ∘ ⇑toFun)

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.

source
theorem UniformFun.postcomp_isUniformEmbedding {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] [UniformSpace γ] {f : γ → β} (hf : IsUniformEmbedding f) :
IsUniformEmbedding (⇑ofFun ∘ (fun (x : α → γ) => f ∘ x) ∘ ⇑toFun)

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.

source
theorem UniformFun.comap_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {f : γ → β} :
uniformSpace α γ = UniformSpace.comap (fun (x : α → γ) => f ∘ x) (uniformSpace α β)

If `u` is a uniform structures on `β` and `f : γ → β`, then `𝒰(α, γ, comap f u) = comap (fun g ↦ f ∘ g) 𝒰(α, γ, u₁)`.

source
theorem UniformFun.postcomp_uniformContinuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] [UniformSpace γ] {f : γ → β} (hf : UniformContinuous f) :
UniformContinuous (⇑ofFun ∘ (fun (x : α → γ) => f ∘ x) ∘ ⇑toFun)

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.

source
def UniformFun.congrRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] [UniformSpace γ] (e : γ ≃ᵤ β) :
UniformFun α γ ≃ᵤ UniformFun α β

Turn a uniform isomorphism `γ ≃ᵤ β` into a uniform isomorphism `(α →ᵤ γ) ≃ᵤ (α →ᵤ β)` by post-composing.

Equations

- UniformFun.congrRight e = { toEquiv := Equiv.piCongrRight fun (x : α) => e.toEquiv, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
theorem UniformFun.precomp_uniformContinuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {f : γ → α} :
UniformContinuous fun (g : UniformFun α β) => ofFun (toFun g ∘ f)

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.

source
def UniformFun.congrLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] (e : γ ≃ α) :
UniformFun γ β ≃ᵤ UniformFun α β

Turn a bijection `γ ≃ α` into a uniform isomorphism `(γ →ᵤ β) ≃ᵤ (α →ᵤ β)` by pre-composing.

Equations

- UniformFun.congrLeft e = { toEquiv := e.arrowCongr (Equiv.refl β), uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
theorem UniformFun.uniformContinuous_toFun {α : Type u_1} {β : Type u_2} [UniformSpace β] :
UniformContinuous ⇑toFun

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.

source
instance UniformFun.instT2Space {α : Type u_1} {β : Type u_2} [UniformSpace β] [T2Space β] :
T2Space (UniformFun α β)

The topology of uniform convergence is T₂.

source
theorem UniformFun.tendsto_iff_tendstoUniformly {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : Filter ι} [UniformSpace β] {F : ι → UniformFun α β} {f : UniformFun α β} :
Filter.Tendsto F p (nhds f) ↔ TendstoUniformly (⇑toFun ∘ F) (toFun f) p

The topology of uniform convergence indeed gives the same notion of convergence as `TendstoUniformly`.

source
def UniformFun.uniformEquivProdArrow {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] [UniformSpace γ] :
UniformFun α (β × γ) ≃ᵤ UniformFun α β × UniformFun α γ

The natural bijection between `α → β × γ` and `(α → β) × (α → γ)`, upgraded to a uniform isomorphism between `α →ᵤ β × γ` and `(α →ᵤ β) × (α →ᵤ γ)`.

Equations

- UniformFun.uniformEquivProdArrow = (Equiv.arrowProdEquivProdArrow α (fun (a : α) => β) fun (a : α) => γ).toUniformEquivOfIsUniformInducing ⋯

Instances For

source
def UniformFun.uniformEquivPiComm (α : Type u_1) {ι : Type u_4} (δ : ι → Type u_5) [(i : ι) → UniformSpace (δ i)] :
UniformFun α ((i : ι) → δ i) ≃ᵤ ((i : ι) → UniformFun α (δ i))

The natural bijection between `α → Π i, δ i` and `Π i, α → δ i`, upgraded to a uniform isomorphism between `α →ᵤ (Π i, δ i)` and `Π i, α →ᵤ δ i`.

Equations

- UniformFun.uniformEquivPiComm α δ = (Equiv.piComm fun (a : α) => δ).toUniformEquivOfIsUniformInducing ⋯

Instances For

source
theorem UniformFun.isClosed_setOf_continuous (α : Type u_1) {β : Type u_2} [UniformSpace β] [TopologicalSpace α] :
IsClosed {f : UniformFun α β | Continuous (toFun f)}

The set of continuous functions is closed in the uniform convergence topology. This is a simple wrapper over `TendstoUniformly.continuous`.

source
theorem UniformFun.uniformSpace_eq_inf_precomp_of_cover {α : Type u_1} (β : Type u_2) [UniformSpace β] {δ₁ : Type u_6} {δ₂ : Type u_7} (φ₁ : δ₁ → α) (φ₂ : δ₂ → α) (h_cover : Set.range φ₁ ∪ Set.range φ₂ = Set.univ) :
uniformSpace α β = UniformSpace.comap (⇑ofFun ∘ (fun (x : α → β) => x ∘ φ₁) ∘ ⇑toFun) (uniformSpace δ₁ β) ⊓ UniformSpace.comap (⇑ofFun ∘ (fun (x : α → β) => x ∘ φ₂) ∘ ⇑toFun) (uniformSpace δ₂ β)
source
theorem UniformFun.uniformSpace_eq_iInf_precomp_of_cover {α : Type u_1} (β : Type u_2) {ι : Type u_4} [UniformSpace β] {δ : ι → Type u_6} (φ : (i : ι) → δ i → α) (h_cover : ∃ (I : Set ι), I.Finite ∧ ⋃ i ∈ I, Set.range (φ i) = Set.univ) :
uniformSpace α β = ⨅ (i : ι), UniformSpace.comap (⇑ofFun ∘ (fun (x : α → β) => x ∘ φ i) ∘ ⇑toFun) (uniformSpace (δ i) β)
source
def UniformOnFun.gen {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)) (S : Set α) (V : Set (β × β)) :
Set (UniformOnFun α β 𝔖 × UniformOnFun α β 𝔖)

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.

Equations

- UniformOnFun.gen 𝔖 S V = {uv : UniformOnFun α β 𝔖 × UniformOnFun α β 𝔖 | ∀ x ∈ S, ((UniformOnFun.toFun 𝔖) uv.1 x, (UniformOnFun.toFun 𝔖) uv.2 x) ∈ V}

Instances For

source
theorem UniformOnFun.gen_eq_preimage_restrict {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} (S : Set α) (V : Set (β × β)) :
UniformOnFun.gen 𝔖 S V = Prod.map (S.restrict ∘ ⇑UniformFun.toFun) (S.restrict ∘ ⇑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β V

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`.

source
theorem UniformOnFun.gen_mono {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {S S' : Set α} {V V' : Set (β × β)} (hS : S' ⊆ S) (hV : V ⊆ V') :
UniformOnFun.gen 𝔖 S V ⊆ UniformOnFun.gen 𝔖 S' V'

`UniformOnFun.gen` is antitone in the first argument and monotone in the second.

source
theorem UniformOnFun.isBasis_gen {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)) (h : 𝔖.Nonempty) (h' : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) 𝔖) (𝓑 : FilterBasis (β × β)) :
Filter.IsBasis (fun (SV : Set α × Set (β × β)) => SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓑) fun (SV : Set α × Set (β × β)) => UniformOnFun.gen 𝔖 SV.1 SV.2

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 `α →ᵤ[𝔖] β`.

source
instance UniformOnFun.uniformSpace (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) :
UniformSpace (UniformOnFun α β 𝔖)

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 `β`.

Equations

- UniformOnFun.uniformSpace α β 𝔖 = ⨅ s ∈ 𝔖, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(UniformOnFun.toFun 𝔖)) (UniformFun.uniformSpace (↑s) β)

source
instance UniformOnFun.topologicalSpace (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) :
TopologicalSpace (UniformOnFun α β 𝔖)

Topology of `𝔖`-convergence, i.e uniform convergence on the elements of `𝔖`, declared as an instance on `α →ᵤ[𝔖] β`.

Equations

- UniformOnFun.topologicalSpace α β 𝔖 = (UniformOnFun.uniformSpace α β 𝔖).toTopologicalSpace

source
theorem UniformOnFun.topologicalSpace_eq (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) :
topologicalSpace α β 𝔖 = ⨅ s ∈ 𝔖, TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.topologicalSpace (↑s) β)

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.

source
theorem UniformOnFun.hasBasis_uniformity_of_basis_aux₁ (α : Type u_1) (β : Type u_2) {ι : Type u_4} [UniformSpace β] (𝔖 : Set (Set α)) {p : ι → Prop} {s : ι → Set (β × β)} (hb : (uniformity β).HasBasis p s) (S : Set α) :
(uniformity (UniformOnFun α β 𝔖)).HasBasis p fun (i : ι) => UniformOnFun.gen 𝔖 S (s i)
source
theorem UniformOnFun.hasBasis_uniformity_of_basis_aux₂ (α : Type u_1) (β : Type u_2) {ι : Type u_4} [UniformSpace β] (𝔖 : Set (Set α)) (h : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) 𝔖) {p : ι → Prop} {s : ι → Set (β × β)} (hb : (uniformity β).HasBasis p s) :
DirectedOn ((fun (s : Set α) => UniformSpace.comap s.restrict (UniformFun.uniformSpace (↑s) β)) ⁻¹'o GE.ge) 𝔖
source
theorem UniformOnFun.hasBasis_uniformity_of_basis (α : Type u_1) (β : Type u_2) {ι : Type u_4} [UniformSpace β] (𝔖 : Set (Set α)) (h : 𝔖.Nonempty) (h' : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) 𝔖) {p : ι → Prop} {s : ι → Set (β × β)} (hb : (uniformity β).HasBasis p s) :
(uniformity (UniformOnFun α β 𝔖)).HasBasis (fun (Si : Set α × ι) => Si.1 ∈ 𝔖 ∧ p Si.2) fun (Si : Set α × ι) => UniformOnFun.gen 𝔖 Si.1 (s Si.2)

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.

source
theorem UniformOnFun.hasBasis_uniformity (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) (h : 𝔖.Nonempty) (h' : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) 𝔖) :
(uniformity (UniformOnFun α β 𝔖)).HasBasis (fun (SV : Set α × Set (β × β)) => SV.1 ∈ 𝔖 ∧ SV.2 ∈ uniformity β) fun (SV : Set α × Set (β × β)) => UniformOnFun.gen 𝔖 SV.1 SV.2

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.

source
theorem UniformOnFun.hasBasis_uniformity_of_covering_of_basis {α : Type u_1} {β : Type u_2} [UniformSpace β] (𝔖 : Set (Set α)) {ι : Type u_5} {ι' : Type u_6} [Nonempty ι] {t : ι → Set α} {p : ι' → Prop} {V : ι' → Set (β × β)} (ht : ∀ (i : ι), t i ∈ 𝔖) (hdir : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) t) (hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i) (hb : (uniformity β).HasBasis p V) :
(uniformity (UniformOnFun α β 𝔖)).HasBasis (fun (i : ι × ι') => p i.2) fun (i : ι × ι') => UniformOnFun.gen 𝔖 (t i.1) (V i.2)

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 `α →ᵤ[𝔖] β`.

source
theorem UniformOnFun.hasAntitoneBasis_uniformity {α : Type u_1} {β : Type u_2} [UniformSpace β] (𝔖 : Set (Set α)) {ι : Type u_5} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {t : ι → Set α} {V : ι → Set (β × β)} (ht : ∀ (n : ι), t n ∈ 𝔖) (hmono : Monotone t) (hex : ∀ s ∈ 𝔖, ∃ (n : ι), s ⊆ t n) (hb : (uniformity β).HasAntitoneBasis V) :
(uniformity (UniformOnFun α β 𝔖)).HasAntitoneBasis fun (n : ι) => UniformOnFun.gen 𝔖 (t n) (V n)

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 `α →ᵤ[𝔖] β`.

source
theorem UniformOnFun.isCountablyGenerated_uniformity {α : Type u_1} {β : Type u_2} [UniformSpace β] (𝔖 : Set (Set α)) [(uniformity β).IsCountablyGenerated] {t : ℕ → Set α} (ht : ∀ (n : ℕ), t n ∈ 𝔖) (hmono : Monotone t) (hex : ∀ s ∈ 𝔖, ∃ (n : ℕ), s ⊆ t n) :
(uniformity (UniformOnFun α β 𝔖)).IsCountablyGenerated
source
theorem UniformOnFun.hasBasis_nhds_of_basis (α : Type u_1) (β : Type u_2) {ι : Type u_4} [UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖) (h : 𝔖.Nonempty) (h' : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) 𝔖) {p : ι → Prop} {s : ι → Set (β × β)} (hb : (uniformity β).HasBasis p s) :
(nhds f).HasBasis (fun (Si : Set α × ι) => Si.1 ∈ 𝔖 ∧ p Si.2) fun (Si : Set α × ι) => {g : UniformOnFun α β 𝔖 | (g, f) ∈ UniformOnFun.gen 𝔖 Si.1 (s Si.2)}

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 `𝓤 β`.

source
theorem UniformOnFun.hasBasis_nhds (α : Type u_1) (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖) (h : 𝔖.Nonempty) (h' : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) 𝔖) :
(nhds f).HasBasis (fun (SV : Set α × Set (β × β)) => SV.1 ∈ 𝔖 ∧ SV.2 ∈ uniformity β) fun (SV : Set α × Set (β × β)) => {g : UniformOnFun α β 𝔖 | (g, f) ∈ UniformOnFun.gen 𝔖 SV.1 SV.2}

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.

source
theorem UniformOnFun.uniformContinuous_restrict (α : Type u_1) (β : Type u_2) {s : Set α} [UniformSpace β] (𝔖 : Set (Set α)) (h : s ∈ 𝔖) :
UniformContinuous (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖))

If `S ∈ 𝔖`, then the restriction to `S` is a uniformly continuous map from `α →ᵤ[𝔖] β` to `↥S →ᵤ β`.

source
theorem UniformOnFun.isUniformEmbedding_toFun_finite (α : Type u_1) (β : Type u_2) [UniformSpace β] :
IsUniformEmbedding ⇑(toFun {s : Set α | s.Finite})
source
theorem UniformOnFun.isEmbedding_toFun_finite (α : Type u_1) (β : Type u_2) [UniformSpace β] :
Topology.IsEmbedding ⇑(toFun {s : Set α | s.Finite})
source
theorem UniformOnFun.uniformity_eq_of_basis {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) {ι : Sort u_5} {p : ι → Prop} {V : ι → Set (β × β)} (h : (uniformity β).HasBasis p V) :
uniformity (UniformOnFun α β 𝔖) = ⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), Filter.principal (UniformOnFun.gen 𝔖 s (V i))

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.

source
theorem UniformOnFun.uniformity_eq {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) :
uniformity (UniformOnFun α β 𝔖) = ⨅ s ∈ 𝔖, ⨅ V ∈ uniformity β, Filter.principal (UniformOnFun.gen 𝔖 s V)
source
theorem UniformOnFun.gen_mem_uniformity {α : Type u_1} (β : Type u_2) {s : Set α} [UniformSpace β] (𝔖 : Set (Set α)) (hs : s ∈ 𝔖) {V : Set (β × β)} (hV : V ∈ uniformity β) :
UniformOnFun.gen 𝔖 s V ∈ uniformity (UniformOnFun α β 𝔖)
source
theorem UniformOnFun.nhds_eq_of_basis {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) {ι : Sort u_5} {p : ι → Prop} {V : ι → Set (β × β)} (h : (uniformity β).HasBasis p V) (f : UniformOnFun α β 𝔖) :
nhds f = ⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), Filter.principal {g : UniformOnFun α β 𝔖 | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V i}

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.

source
theorem UniformOnFun.nhds_eq {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖) :
nhds f = ⨅ s ∈ 𝔖, ⨅ V ∈ uniformity β, Filter.principal {g : UniformOnFun α β 𝔖 | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V}
source
theorem UniformOnFun.gen_mem_nhds {α : Type u_1} (β : Type u_2) {s : Set α} [UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖) (hs : s ∈ 𝔖) {V : Set (β × β)} (hV : V ∈ uniformity β) :
{g : UniformOnFun α β 𝔖 | ∀ x ∈ s, ((toFun 𝔖) f x, (toFun 𝔖) g x) ∈ V} ∈ nhds f
source
theorem UniformOnFun.uniformContinuous_ofUniformFun {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) :
UniformContinuous fun (f : UniformFun α β) => (ofFun 𝔖) (UniformFun.toFun f)
source
def UniformOnFun.uniformEquivUniformFun {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) (h : Set.univ ∈ 𝔖) :
UniformOnFun α β 𝔖 ≃ᵤ UniformFun α β

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

Here we formulate it as a `UniformEquiv`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem UniformOnFun.uniformContinuous_ofFun_toFun {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 𝔗 : Set (Set α)) (h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T) :
UniformContinuous (⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖))

If `𝔖` and `𝔗` are families of sets in `α`, then the identity map `(α →ᵤ[𝔗] β) → (α →ᵤ[𝔖] β)` is uniformly continuous if every `s ∈ 𝔖` is contained in a finite union of elements of `𝔗`.

With more API around `Order.Ideal`, this could be phrased in that language instead.

source
theorem UniformOnFun.mono {α : Type u_1} {γ : Type u_3} ⦃u₁ u₂ : UniformSpace γ⦄ (hu : u₁ ≤ u₂) ⦃𝔖₁ 𝔖₂ : Set (Set α)⦄ (h𝔖 : 𝔖₂ ⊆ 𝔖₁) :
uniformSpace α γ 𝔖₁ ≤ uniformSpace α γ 𝔖₂

Let `u₁`, `u₂` be two uniform structures on `γ` and `𝔖₁ 𝔖₂ : Set (Set α)`. If `u₁ ≤ u₂` and `𝔖₂ ⊆ 𝔖₁` then `𝒱(α, γ, 𝔖₁, u₁) ≤ 𝒱(α, γ, 𝔖₂, u₂)`.

source
theorem UniformOnFun.uniformContinuous_eval_of_mem {α : Type u_1} (β : Type u_2) {s : Set α} [UniformSpace β] (𝔖 : Set (Set α)) {x : α} (hxs : x ∈ s) (hs : s ∈ 𝔖) :
UniformContinuous (Function.eval x ∘ ⇑(toFun 𝔖))

If `x : α` is in some `S ∈ 𝔖`, then evaluation at `x` is uniformly continuous on `α →ᵤ[𝔖] β`.

source
theorem UniformOnFun.uniformContinuous_eval_of_mem_sUnion {α : Type u_1} (β : Type u_2) [UniformSpace β] (𝔖 : Set (Set α)) {x : α} (hx : x ∈ ⋃₀ 𝔖) :
UniformContinuous (Function.eval x ∘ ⇑(toFun 𝔖))
source
theorem UniformOnFun.uniformContinuous_eval {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} (h : ⋃₀ 𝔖 = Set.univ) (x : α) :
UniformContinuous (Function.eval x ∘ ⇑(toFun 𝔖))
source
theorem UniformOnFun.iInf_eq {α : Type u_1} {γ : Type u_3} {ι : Type u_4} {𝔖 : Set (Set α)} {u : ι → UniformSpace γ} :
uniformSpace α γ 𝔖 = ⨅ (i : ι), uniformSpace α γ 𝔖

If `u` is a family of uniform structures on `γ`, then `𝒱(α, γ, 𝔖, (⨅ i, u i)) = ⨅ i, 𝒱(α, γ, 𝔖, u i)`.

source
theorem UniformOnFun.inf_eq {α : Type u_1} {γ : Type u_3} {𝔖 : Set (Set α)} {u₁ u₂ : UniformSpace γ} :
uniformSpace α γ 𝔖 = uniformSpace α γ 𝔖 ⊓ uniformSpace α γ 𝔖

If `u₁` and `u₂` are two uniform structures on `γ`, then `𝒱(α, γ, 𝔖, u₁ ⊓ u₂) = 𝒱(α, γ, 𝔖, u₁) ⊓ 𝒱(α, γ, 𝔖, u₂)`.

source
theorem UniformOnFun.comap_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} {f : γ → β} :
uniformSpace α γ 𝔖 = UniformSpace.comap (fun (x : α → γ) => f ∘ x) (uniformSpace α β 𝔖)

If `u` is a uniform structure on `β` and `f : γ → β`, then `𝒱(α, γ, 𝔖, comap f u) = comap (fun g ↦ f ∘ g) 𝒱(α, γ, 𝔖, u₁)`.

source
theorem UniformOnFun.postcomp_uniformContinuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} [UniformSpace γ] {f : γ → β} (hf : UniformContinuous f) :
UniformContinuous (⇑(ofFun 𝔖) ∘ (fun (x : α → γ) => f ∘ x) ∘ ⇑(toFun 𝔖))

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.

source
theorem UniformOnFun.postcomp_isUniformInducing {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} [UniformSpace γ] {f : γ → β} (hf : IsUniformInducing f) :
IsUniformInducing (⇑(ofFun 𝔖) ∘ (fun (x : α → γ) => f ∘ x) ∘ ⇑(toFun 𝔖))

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.

source
theorem UniformOnFun.postcomp_isUniformEmbedding {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} [UniformSpace γ] {f : γ → β} (hf : IsUniformEmbedding f) :
IsUniformEmbedding (⇑(ofFun 𝔖) ∘ (fun (x : α → γ) => f ∘ x) ∘ ⇑(toFun 𝔖))

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.

source
def UniformOnFun.congrRight {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} [UniformSpace γ] (e : γ ≃ᵤ β) :
UniformOnFun α γ 𝔖 ≃ᵤ UniformOnFun α β 𝔖

Turn a uniform isomorphism `γ ≃ᵤ β` into a uniform isomorphism `(α →ᵤ[𝔖] γ) ≃ᵤ (α →ᵤ[𝔖] β)` by post-composing.

Equations

- UniformOnFun.congrRight e = { toEquiv := Equiv.piCongrRight fun (_a : α) => e.toEquiv, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
theorem UniformOnFun.precomp_uniformContinuous {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} {𝔗 : Set (Set γ)} {f : γ → α} (hf : Set.MapsTo (fun (x : Set γ) => f '' x) 𝔗 𝔖) :
UniformContinuous fun (g : UniformOnFun α β 𝔖) => (ofFun 𝔗) ((toFun 𝔖) g ∘ f)

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 `𝔖`.

source
def UniformOnFun.congrLeft {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} {𝔗 : Set (Set γ)} (e : γ ≃ α) (he : 𝔗 ⊆ Set.image ⇑e ⁻¹' 𝔖) (he' : 𝔖 ⊆ Set.preimage ⇑e ⁻¹' 𝔗) :
UniformOnFun γ β 𝔗 ≃ᵤ UniformOnFun α β 𝔖

Turn a bijection `e : γ ≃ α` such that we have both `∀ T ∈ 𝔗, e '' T ∈ 𝔖` and `∀ S ∈ 𝔖, e ⁻¹' S ∈ 𝔗` into a uniform isomorphism `(γ →ᵤ[𝔗] β) ≃ᵤ (α →ᵤ[𝔖] β)` by pre-composing.

Equations

- UniformOnFun.congrLeft e he he' = { toEquiv := e.arrowCongr (Equiv.refl β), uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

Instances For

source
theorem UniformOnFun.t2Space_of_covering {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [T2Space β] (h : ⋃₀ 𝔖 = Set.univ) :
T2Space (UniformOnFun α β 𝔖)

If `𝔖` covers `α`, then the topology of `𝔖`-convergence is T₂.

source
theorem UniformOnFun.uniformContinuous_restrict_toFun {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} :
UniformContinuous ((⋃₀ 𝔖).restrict ∘ ⇑(toFun 𝔖))

The restriction map from `α →ᵤ[𝔖] β` to `⋃₀ 𝔖 → β` is uniformly continuous.

source
theorem UniformOnFun.isUniformInducing_pi_restrict {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} :
IsUniformInducing fun (f : UniformOnFun α β 𝔖) (s : ↑𝔖) => UniformFun.ofFun ((↑s).restrict ((toFun 𝔖) f))

The map sending a function `f : α →ᵤ[𝔖] β` to the family of restrictions of `f` to each `s ∈ 𝔖` (each coordinate equipped with its respective uniform structure `s →ᵤ β`) induces the uniformity on `α →ᵤ[𝔖] β`.

source
theorem UniformOnFun.uniformContinuous_toFun {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} (h : ⋃₀ 𝔖 = Set.univ) :
UniformContinuous ⇑(toFun 𝔖)

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.

source
theorem UniformOnFun.continuousAt_eval₂ {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [TopologicalSpace α] {f : UniformOnFun α β 𝔖} {x : α} (h𝔖 : ∃ V ∈ 𝔖, V ∈ nhds x) (hc : ContinuousAt ((toFun 𝔖) f) x) :
ContinuousAt (fun (fx : UniformOnFun α β 𝔖 × α) => (toFun 𝔖) fx.1 fx.2) (f, x)

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)`.

source
theorem UniformOnFun.continuousOn_eval₂ {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [TopologicalSpace α] (h𝔖 : ∀ (x : α), ∃ V ∈ 𝔖, V ∈ nhds x) :
ContinuousOn (fun (fx : UniformOnFun α β 𝔖 × α) => (toFun 𝔖) fx.1 fx.2) {fx : UniformOnFun α β 𝔖 × α | ContinuousAt ((toFun 𝔖) fx.1) fx.2}

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`.

source
theorem UniformOnFun.tendsto_iff_tendstoUniformlyOn {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : Filter ι} [UniformSpace β] {𝔖 : Set (Set α)} {F : ι → UniformOnFun α β 𝔖} {f : UniformOnFun α β 𝔖} :
Filter.Tendsto F p (nhds f) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(toFun 𝔖) ∘ F) ((toFun 𝔖) f) p s

Convergence in the topology of `𝔖`-convergence means uniform convergence on `S` (in the sense of `TendstoUniformlyOn`) for all `S ∈ 𝔖`.

source
theorem UniformOnFun.continuous_rng_iff {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} {X : Type u_5} [TopologicalSpace X] {f : X → UniformOnFun α β 𝔖} :
Continuous f ↔ ∀ s ∈ 𝔖, Continuous (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖) ∘ f)
source
instance UniformOnFun.instCompleteSpace {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [CompleteSpace β] :
CompleteSpace (UniformOnFun α β 𝔖)
source
def UniformOnFun.uniformEquivProdArrow {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace β] {𝔖 : Set (Set α)} [UniformSpace γ] :
UniformOnFun α (β × γ) 𝔖 ≃ᵤ UniformOnFun α β 𝔖 × UniformOnFun α γ 𝔖

The natural bijection between `α → β × γ` and `(α → β) × (α → γ)`, upgraded to a uniform isomorphism between `α →ᵤ[𝔖] β × γ` and `(α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ)`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def UniformOnFun.uniformEquivPiComm {α : Type u_1} {ι : Type u_4} (𝔖 : Set (Set α)) (δ : ι → Type u_5) [(i : ι) → UniformSpace (δ i)] :
UniformOnFun α ((i : ι) → δ i) 𝔖 ≃ᵤ ((i : ι) → UniformOnFun α (δ i) 𝔖)

The natural bijection between `α → Π i, δ i` and `Π i, α → δ i`, upgraded to a uniform isomorphism between `α →ᵤ[𝔖] (Π i, δ i)` and `Π i, α →ᵤ[𝔖] δ i`.

Equations

- UniformOnFun.uniformEquivPiComm 𝔖 δ = (Equiv.piComm fun (a : α) => δ).toUniformEquivOfIsUniformInducing ⋯

Instances For

source
theorem UniformOnFun.isClosed_setOf_continuous {α : Type u_1} {β : Type u_2} [UniformSpace β] {𝔖 : Set (Set α)} [TopologicalSpace α] (h : Topology.IsCoherentWith 𝔖) :
IsClosed {f : UniformOnFun α β 𝔖 | Continuous ((toFun 𝔖) f)}

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 `𝔖`.

source
theorem UniformOnFun.uniformSpace_eq_inf_precomp_of_cover {α : Type u_1} {β : Type u_2} [UniformSpace β] (𝔖 : Set (Set α)) {δ₁ : Type u_5} {δ₂ : Type u_6} (φ₁ : δ₁ → α) (φ₂ : δ₂ → α) (𝔗₁ : Set (Set δ₁)) (𝔗₂ : Set (Set δ₂)) (h_image₁ : Set.MapsTo (fun (x : Set δ₁) => φ₁ '' x) 𝔗₁ 𝔖) (h_image₂ : Set.MapsTo (fun (x : Set δ₂) => φ₂ '' x) 𝔗₂ 𝔖) (h_preimage₁ : Set.MapsTo (fun (x : Set α) => φ₁ ⁻¹' x) 𝔖 𝔗₁) (h_preimage₂ : Set.MapsTo (fun (x : Set α) => φ₂ ⁻¹' x) 𝔖 𝔗₂) (h_cover : ∀ S ∈ 𝔖, S ⊆ Set.range φ₁ ∪ Set.range φ₂) :
uniformSpace α β 𝔖 = UniformSpace.comap (⇑(ofFun 𝔗₁) ∘ (fun (x : α → β) => x ∘ φ₁) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₁ β 𝔗₁) ⊓ UniformSpace.comap (⇑(ofFun 𝔗₂) ∘ (fun (x : α → β) => x ∘ φ₂) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₂ β 𝔗₂)
source
theorem UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] (𝔖 : Set (Set α)) {δ : ι → Type u_5} (φ : (i : ι) → δ i → α) (𝔗 : (i : ι) → Set (Set (δ i))) (h_image : ∀ (i : ι), Set.MapsTo (fun (x : Set (δ i)) => φ i '' x) (𝔗 i) 𝔖) (h_preimage : ∀ (i : ι), Set.MapsTo (fun (x : Set α) => φ i ⁻¹' x) 𝔖 (𝔗 i)) (h_cover : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, Set.range (φ i)) :
uniformSpace α β 𝔖 = ⨅ (i : ι), UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun (x : α → β) => x ∘ φ i) ∘ ⇑(toFun 𝔖)) (uniformSpace (δ i) β (𝔗 i))
source
instance UniformFun.instCompleteSpace {α : Type u_1} {β : Type u_2} [UniformSpace β] [CompleteSpace β] :
CompleteSpace (UniformFun α β)
source
theorem UniformContinuousOn.comp_tendstoUniformly {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [UniformSpace β] [UniformSpace γ] {p : Filter ι} {s : Set β} {F : ι → α → β} {f : α → β} {g : β → γ} (hF : ∀ (i : ι) (x : α), F i x ∈ s) (hf : ∀ (x : α), f x ∈ s) (hg : UniformContinuousOn g s) (h : TendstoUniformly F f p) :
TendstoUniformly (fun (i : ι) (x : α) => g (F i x)) (fun (x : α) => g (f x)) p

Composing on the left by a uniformly continuous function preserves uniform convergence

source
theorem UniformContinuousOn.comp_tendstoUniformly_eventually {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [UniformSpace β] [UniformSpace γ] {p : Filter ι} {s : Set β} {F : ι → α → β} {f : α → β} {g : β → γ} (hF : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s) (hf : ∀ (x : α), f x ∈ s) (hg : UniformContinuousOn g s) (h : TendstoUniformly F f p) :
TendstoUniformly (fun (i : ι) (x : α) => g (F i x)) (fun (x : α) => g (f x)) p
source
theorem UniformContinuousOn.comp_tendstoUniformlyOn_eventually {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [UniformSpace β] [UniformSpace γ] {p : Filter ι} {s : Set β} {F : ι → α → β} {f : α → β} {t : Set α} (hF : ∀ᶠ (i : ι) in p, ∀ x ∈ t, F i x ∈ s) (hf : ∀ x ∈ t, f x ∈ s) {g : β → γ} (hg : UniformContinuousOn g s) (h : TendstoUniformlyOn F f p t) :
TendstoUniformlyOn (fun (i : ι) (x : α) => g (F i x)) (fun (x : α) => g (f x)) p t