UniformFun.hasBasis_uniformity_of_basis
theorem UniformFun.hasBasis_uniformity_of_basis :
∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β] {ι : Sort u_5} {p : ι → Prop} {s : ι → Set (β × β)},
(uniformity β).HasBasis p s → (uniformity (UniformFun α β)).HasBasis p (UniformFun.gen α β ∘ s)
This theorem asserts that the uniformity of the uniform space of functions from `α` to `β` (`α →ᵤ β`), has a filter basis `{(f, g) | ∀ x, (f x, g x) ∈ V}` for any `V` belonging to a basis `𝓑` of the uniformity `𝓤 β`. This filter basis is created through the operation `UniformFun.gen α β ∘ s` which maps every `s` in `𝓑` to a set of pairs of functions `(f, g)` such that for every `x` in `α`, the pair `(f(x), g(x))` belongs to `V`. This statement holds true especially when `𝓑` is the set of basis elements of the uniformity `𝓤 β`, i.e., `𝓑 = (𝓤 β).as_basis`.
More concisely: The uniformity of functions from `α` to `β` has a filter basis consisting of pairs of functions `(f, g)` such that for all `x in α`, `(f x, g x)` belongs to any given basis element of the uniformity of `β`.
|
UniformOnFun.iInf_eq
theorem UniformOnFun.iInf_eq :
∀ {α : Type u_1} {γ : Type u_3} {ι : Type u_4} {𝔖 : Set (Set α)} {u : ι → UniformSpace γ},
UniformOnFun.uniformSpace α γ 𝔖 = ⨅ i, UniformOnFun.uniformSpace α γ 𝔖
This theorem states that for any types `α`, `γ`, and `ι`, for any set `𝔖` of subsets of `α`, and for any family `u` of uniform structures on `γ`, the uniform space constructed from `α`, `γ`, `𝔖`, and the infimum of the family `u` is equal to the infimum of the uniform spaces constructed from `α`, `γ`, `𝔖`, and each member of the family `u`. In other words, the infimum operation commutes with the construction of uniform spaces.
More concisely: The infimum of uniform structures on a pair of types and a set of subsets is commutative with the construction of uniform spaces from those types, sets, and uniform structures.
|
UniformOnFun.isBasis_gen
theorem UniformOnFun.isBasis_gen :
∀ {α : Type u_1} {β : Type u_2} (𝔖 : Set (Set α)),
𝔖.Nonempty →
DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖 →
∀ (𝓑 : FilterBasis (β × β)),
Filter.IsBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓑) fun SV => UniformOnFun.gen 𝔖 SV.1 SV.2
This theorem states that, given a non-empty and directed set `𝔖` of subsets of a type `α` and a filter basis `𝓑` on pairs of a type `β`, the family of sets produced by the function `UniformOnFun.gen 𝔖 S V` for each `S` in `𝔖` and `V` in `𝔑` forms a filter basis on pairs of functions from `α` to `β` that are uniform with respect to `𝔖`. Essentially, if we have a set `𝔖` that is nonempty and directed, and a filter basis `𝓑`, we can generate a new filter basis on uniform functions from `α` to `β`. Furthermore, if `𝓑` forms a basis for the uniformity `𝓤 β`, then this new filter would correspond to the uniformity of `α →ᵤ[𝔖] β`.
More concisely: Given a non-empty and directed set `𝔖` of subsets of `α` and a filter basis `𝓑` on pairs of functions from `α` to `β`, the family of sets generated by `UniformOnFun.gen 𝔖 S V` forms a filter basis on uniform functions from `α` to `β` with respect to `𝔖`. If `𝓑` is a basis for the uniformity of `β`, this new filter corresponds to the uniformity of `α →[𝔖] β`.
|
UniformOnFun.topologicalSpace_eq
theorem UniformOnFun.topologicalSpace_eq :
∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β] (𝔖 : Set (Set α)),
UniformOnFun.topologicalSpace α β 𝔖 =
⨅ s ∈ 𝔖,
TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(UniformOnFun.toFun 𝔖))
(UniformFun.topologicalSpace (↑s) β)
The theorem `UniformOnFun.topologicalSpace_eq` states that for any types `α` and `β` where `β` is a uniform space, and for any set `𝔖` of subsets of `α`, the topology of `𝔖`-convergence (i.e., uniform convergence on the elements of `𝔖`) is equal to the infimum, for each subset `S` in `𝔖`, of the topology induced by mapping the restriction to `S` to the topology of uniform convergence on `S`. In other words, the topology of `𝔖`-convergence is the coarsest topology such that all these restriction maps are continuous.
More concisely: The topology of uniform convergence on a set of subsets of a uniform space is equal to the infimum of the topologies induced by restricting to each subset and mapping to the uniform convergence topology on that subset.
|
UniformOnFun.gen_mono
theorem UniformOnFun.gen_mono :
∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} {S S' : Set α} {V V' : Set (β × β)},
S' ⊆ S → V ⊆ V' → UniformOnFun.gen 𝔖 S V ⊆ UniformOnFun.gen 𝔖 S' V'
The theorem `UniformOnFun.gen_mono` states that for any sets `S`, `S'` of type `α`, and `V`, `V'` of type `(β × β)`, and a family `𝔖 : Set (Set α)`, if `S'` is a subset of `S` and `V` is a subset of `V'`, then the set of pairs of functions characterized by `UniformOnFun.gen 𝔖 S V` is a subset of the set characterized by `UniformOnFun.gen 𝔖 S' V'`. In other words, this theorem asserts that the `UniformOnFun.gen` function is antitone (order-reversing) in its first argument and monotone (order-preserving) in its second argument.
More concisely: If `S'` is a subset of `S` and `V'` is a superset of `V`, then `UniformOnFun.gen 𝔖 S V` is a subset of `UniformOnFun.gen 𝔖 S' V'`.
|
UniformOnFun.inf_eq
theorem UniformOnFun.inf_eq :
∀ {α : Type u_1} {γ : Type u_3} {𝔖 : Set (Set α)} {u₁ u₂ : UniformSpace γ},
UniformOnFun.uniformSpace α γ 𝔖 = UniformOnFun.uniformSpace α γ 𝔖 ⊓ UniformOnFun.uniformSpace α γ 𝔖
The theorem `UniformOnFun.inf_eq` states that for any types `α` and `γ`, a set `𝔖` of sets of `α`, and two uniform structures `u₁` and `u₂` on `γ`, the uniform structure `𝒱(α, γ, 𝔖, u₁ ⊓ u₂)` produced by the inference rule `UniformOnFun.uniformSpace` is equal to the intersection of the uniform structures `𝒱(α, γ, 𝔖, u₁)` and `𝒱(α, γ, 𝔖, u₂)` generated by `u₁` and `u₂` respectively. This implies that the uniform structure generated by the intersection of two uniform structures on `γ` is the same as the intersection of the uniform structures generated by each of the two.
More concisely: The uniform structure on `α × γ` generated by two uniform structures `u₁` and `u₂` on `γ` is equal to the intersection of the uniform structures generated by each of `u₁` and `u₂` on `α × γ`.
|
UniformOnFun.hasBasis_uniformity
theorem UniformOnFun.hasBasis_uniformity :
∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β] (𝔖 : Set (Set α)),
𝔖.Nonempty →
DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖 →
(uniformity (UniformOnFun α β 𝔖)).HasBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ uniformity β) fun SV =>
UniformOnFun.gen 𝔖 SV.1 SV.2
This theorem states that if we have a nonempty and directed set `𝔖` of subsets of a type `α`, and `β` is a type equipped with a uniform space structure, then the uniformity of functions from `α` to `β` that converge uniformly on some subset in `𝔖`, admits a certain family as a filter basis. Specifically, this family consists of pairs `(f, g)` of functions from `α` to `β`, for which there exists a subset `S` in `𝔖` and a set `V` in the uniformity of `β` such that for every `x` in `S`, the pair `(f x, g x)` belongs to `V`.
More concisely: Given a nonempty and directed set `𝔖` of subsets of `α` and a uniform space `β`, the uniformity of uniformly convergent functions from `α` to `β` on some subset in `𝔖` has a filter basis consisting of pairs of functions `(f, g)` such that there exists an `S` in `𝔖` and a `V` in the uniformity of `β` with `{(fx, gx) | x ∈ S} ⊆ V`.
|
UniformOnFun.postcomp_uniformInducing
theorem UniformOnFun.postcomp_uniformInducing :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {𝔖 : Set (Set α)} [inst_1 : UniformSpace γ]
{f : γ → β},
UniformInducing f → UniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(UniformOnFun.toFun 𝔖))
This theorem states that post-composition by a uniform inducing function is also a uniform inducing function for uniform structures of 𝔖-convergence. More specifically, if we have a function `f` from `γ` to `β` which is uniform inducing, then the function `(fun g ↦ f ∘ g)` that takes a function `g` from `α` to `γ` (considered in the context of 𝔖-convergence) and returns the composition of `f` and `g`, is also uniform inducing. In other words, this theorem establishes the preservation of the uniform inducing property under function composition in the context of 𝔖-convergence.
More concisely: If `f` is a uniformly inducing function from `γ` to `β` in the context of `𝔖`-convergence, then the function `g ↦ f ∘ g` is also a uniformly inducing function from `α` to `β` in the context of `𝔖`-convergence.
|
UniformFun.comap_eq
theorem UniformFun.comap_eq :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {f : γ → β},
UniformFun.uniformSpace α γ = UniformSpace.comap (fun x => f ∘ x) (UniformFun.uniformSpace α β)
The theorem `UniformFun.comap_eq` states that for any types `α`, `β`, and `γ` such that `β` is equipped with a uniform space structure, and for any function `f` from `γ` to `β`, the uniform space of uniform convergence on `α` to `γ` is equivalent to the comap (pre-image under `f`) of the uniform space of uniform convergence on `α` to `β` under the composition operation with `f`. In simpler terms, this theorem relates the notions of uniform convergence and function composition in the context of uniform spaces.
More concisely: For any uniform spaces X, Y, Z, and function f : Z → Y, the uniform convergence of functions from X to Z is equivalent to the uniform convergence of their compositions with f from X to Y.
|
UniformOnFun.tendsto_iff_tendstoUniformlyOn
theorem UniformOnFun.tendsto_iff_tendstoUniformlyOn :
∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : Filter ι} [inst : UniformSpace β] {𝔖 : Set (Set α)}
{F : ι → UniformOnFun α β 𝔖} {f : UniformOnFun α β 𝔖},
Filter.Tendsto F p (nhds f) ↔
∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(UniformOnFun.toFun 𝔖) ∘ F) ((UniformOnFun.toFun 𝔖) f) p s
The theorem `UniformOnFun.tendsto_iff_tendstoUniformlyOn` states that for any types `α`, `β`, and `ι`, any filter `p` on `ι`, any uniform space on `β`, any set `𝔖` of subsets of `α`, any sequence of functions `F` from `ι` to functions from `α` to `β` equipped with the uniform structure and topology of uniform convergence on `𝔖`, and any function `f` from `α` to `β` equipped with the uniform structure and topology of uniform convergence on `𝔖`, the sequence `F` converges to `f` in the filter `p` if and only if for all subsets `s` in `𝔖`, the sequence of functions `F` transformed by `UniformOnFun.toFun 𝔖` converges uniformly on `s` to the function `f` transformed by `UniformOnFun.toFun 𝔖` with respect to the filter `p`. This uniform convergence is defined by the predicate `TendstoUniformlyOn`, meaning that for all sufficiently large `n` and for all `x` in `s`, the pair `(f(x), F(n)(x))` is in any given entourage of the diagonal in the uniform space `β`.
More concisely: For any uniform space on β, sequence of functions from α to β equipped with the uniform structure of uniform convergence on a set 𝔖, function from α to β equipped with the same uniform structure, and filter on ι, the sequence converges to the function in the filter if and only if for all subsets s in 𝔖, the sequence uniformly converges on s to the function with respect to the filter.
|
UniformOnFun.t2Space_of_covering
theorem UniformOnFun.t2Space_of_covering :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {𝔖 : Set (Set α)} [inst_1 : T2Space β],
𝔖.sUnion = Set.univ → T2Space (UniformOnFun α β 𝔖)
This theorem states that if a family of subsets `𝔖` covers the set `α`, then the topology of `𝔖`-convergence is Hausdorff (or `T2`). Here, `T2` is a property of topological spaces that states that for any two distinct points in the space, there exist disjoint open sets containing each point. In terms of the types `α` and `β`, with `β` being equipped with a uniform structure (`UniformSpace β`), and `T2Space β` denoting that `β` is a `T2` space, if the union of all sets in `𝔖` equals the universal set (`𝔖.sUnion = Set.univ`), then the function space from `α` to `β` under the topology of uniform convergence on `𝔖`, denoted as `UniformOnFun α β 𝔖`, is also a `T2Space`.
More concisely: If a family of subsets covering a set endows it with the uniform convergence topology, then the function space becomes a Hausdorff space.
|
UniformOnFun.precomp_uniformContinuous
theorem UniformOnFun.precomp_uniformContinuous :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {𝔖 : Set (Set α)} {𝔗 : Set (Set γ)}
{f : γ → α},
Set.MapsTo (fun x => f '' x) 𝔗 𝔖 →
UniformContinuous fun g => (UniformOnFun.ofFun 𝔗) ((UniformOnFun.toFun 𝔖) g ∘ f)
This theorem, `UniformOnFun.precomp_uniformContinuous`, states that for any types `α`, `β`, and `γ`, and a uniform space on `β`, given a set of sets `𝔖` in `α`, a set of sets `𝔗` in `γ`, and a function `f` from `γ` to `α`, if the image of each set in `𝔗` under function `f` is a member of `𝔖`, then the function mapping each function `g` from `α` to `β` to the composite of `g` and `f`, which is a function from `γ` to `β`, is uniformly continuous. This function is interpreted through the lens of uniformity on sets `𝔖` and `𝔗`.
The note also mentions that it'd work too if for every set in `𝔗`, there exists a set in `𝔖` such that the image of the set in `𝔗` under function `f` is contained within this set in `𝔖`. This will be a free consequence when proving an equality between the uniformities generated by `𝔖` and `𝔖'`, where `𝔖'` is the noncovering bornology generated by `𝔖`.
More concisely: Given uniform spaces on types `α`, `β`, and `γ`, a set of sets `𝔖` in `α`, a set of sets `𝔗` in `γ`, and a function `f` from `γ` to `α` such that the image of each set in `𝔗` under `f` is a member of `𝔖`, the function mapping each function `g` from `α` to `β` to the composite of `g` and `f` is uniformly continuous with respect to the uniformities generated by `𝔖` and `𝔗`.
|
UniformFun.uniformContinuous_eval
theorem UniformFun.uniformContinuous_eval :
∀ {α : Type u_1} (β : Type u_2) [inst : UniformSpace β] (x : α),
UniformContinuous (Function.eval x ∘ ⇑UniformFun.toFun)
This theorem states that the operation of evaluating a uniformly continuous function at a fixed point is itself uniformly continuous. In more detail, for any types `α` and `β` where `β` is equipped with a uniform space structure, and for any fixed element `x` of type `α`, the function which evaluates a uniformly continuous function from `α` to `β` at the point `x` is uniformly continuous. The symbol `∘` represents function composition, and `⇑UniformFun.toFun` is used to convert a uniformly continuous function into a regular function.
More concisely: If `f : α → β` is uniformly continuous and `x ∈ α` is fixed, then the function `g : α → β` defined by `g(y) := f(y)` for all `y ∈ α` is uniformly continuous.
|
UniformFun.isBasis_gen
theorem UniformFun.isBasis_gen :
∀ (α : Type u_1) (β : Type u_2) (𝓑 : Filter (β × β)), Filter.IsBasis (fun V => V ∈ 𝓑) (UniformFun.gen α β) := by
sorry
The theorem `UniformFun.isBasis_gen` states that for any types `α` and `β` and any filter `𝓑` on pairs of `β`, the set of all `UniformFun.gen α β V` where `V` is an element of `𝓑`, forms a filter basis on the space of pairs of uniform functions from `α` to `β`. This is typically applied when `𝓑` is the uniformity of `β` in the context of a `UniformSpace` structure, however it's defined for any filter to facilitate the statement that it has a lower adjoint (as seen in `UniformFun.gc`). Here, `UniformFun.gen α β V` denotes the set of pairs of uniform functions `(f, g)` such that for all `x` in `α`, the pair `(f(x), g(x))` belongs to `V`.
More concisely: For any types `α` and `β` and filter `𝓑` on pairs of `β`, the collection of sets `{UniformFun.gen α β V : V ∈ 𝓑}` forms a filter basis on the space of uniform functions from `α` to `β`.
|
UniformOnFun.uniformContinuous_toFun
theorem UniformOnFun.uniformContinuous_toFun :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {𝔖 : Set (Set α)},
𝔖.sUnion = Set.univ → UniformContinuous ⇑(UniformOnFun.toFun 𝔖)
The theorem `UniformOnFun.uniformContinuous_toFun` states that if a set `𝔖` of subsets of `α` covers the entire set `α` (i.e., the union of all subsets in `𝔖` is equal to the universal set on `α`), then the function `UniformOnFun.toFun`, which converts a function defined on `α` with respect to the uniform structure of `𝔖` to a function defined on `α`, is uniformly continuous. In other words, if `𝔖` covers `α`, the uniform structure induced by convergence on `𝔖` is finer than the structure of pointwise convergence on `α`.
More concisely: If a uniform structure `𝔖` covering `α` induces finer convergence than pointwise convergence on functions defined on `α`, then `UniformOnFun.toFun` mapping functions defined with respect to `𝔖` to functions on `α` is uniformly continuous.
|
UniformOnFun.hasBasis_nhds_of_basis
theorem UniformOnFun.hasBasis_nhds_of_basis :
∀ (α : Type u_1) (β : Type u_2) {ι : Type u_4} [inst : UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖),
𝔖.Nonempty →
DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖 →
∀ {p : ι → Prop} {s : ι → Set (β × β)},
(uniformity β).HasBasis p s →
(nhds f).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
{g | (g, f) ∈ UniformOnFun.gen 𝔖 Si.1 (s Si.2)}
This theorem states that for a function `f` mapping from `α` to `β` with a uniform structure and topology of uniform convergence on a nonempty and directed set `𝔖` of subsets of `α`, the neighborhood filter of `f` admits a family of sets as a filter basis. This family of sets consists of those functions `g` such that for each `x` in a set `S` from `𝔖` and a set `V` from a basis `𝓑` of the uniformity on `β`, the pair `(f x, g x)` belongs to `V`. The theorem requires the existence of a basis for the uniformity on `β` and it holds for all types `α` and `β`, and for all `f` of type `α →ᵤ[𝔖] β`.
More concisely: For a function `f` with uniform structure and topology of uniform convergence on a nonempty and directed set `𝔖` of `α`, the neighborhood filter of `f` has a basis consisting of functions `g` such that `(f x, g x)` is in every `V` from a basis of the uniformity on `β`, for all `x` in each `S` from `𝔖`.
|
UniformFun.precomp_uniformContinuous
theorem UniformFun.precomp_uniformContinuous :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {f : γ → α},
UniformContinuous fun g => UniformFun.ofFun (UniformFun.toFun g ∘ f)
This theorem states that pre-composition with any function is uniformly continuous for the uniform structures of uniform convergence. In more detailed terms, given any function `f` from a type `γ` to a type `α`, the function that takes a uniformly continuous function from `α` to `β` and composes it with `f` (i.e., `(· ∘ f) : (α →ᵤ β) → (γ →ᵤ β)`) is uniformly continuous. This means that if `x` and `y` are points in `γ` that are close to each other, then the function values after composition, `(g ∘ f)(x)` and `(g ∘ f)(y)`, are also close to each other for any uniformly continuous function `g : α →ᵤ β`, regardless of where `x` and `y` are located in `γ`.
More concisely: Given any uniformly continuous function `f : γ → α` and any uniformly continuous function `g : α → β`, the composed function `(g ∘ f) : γ → β` is also uniformly continuous.
|
UniformFun.tendsto_iff_tendstoUniformly
theorem UniformFun.tendsto_iff_tendstoUniformly :
∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : Filter ι} [inst : UniformSpace β] {F : ι → UniformFun α β}
{f : UniformFun α β},
Filter.Tendsto F p (nhds f) ↔ TendstoUniformly (⇑UniformFun.toFun ∘ F) (UniformFun.toFun f) p
This theorem, `UniformFun.tendsto_iff_tendstoUniformly`, states that for any types `α`, `β`, and `ι`, any filter `p` over `ι`, any uniform space structure on `β`, any sequence of functions `F` from `ι` to `UniformFun α β`, and any function `f` of type `UniformFun α β`, the notion of convergence given by `Filter.Tendsto` towards the neighborhood filter of `f` is equivalent to the uniform convergence of the sequence of functions represented by `F` to the function represented by `f` with respect to the filter `p`. In other words, a sequence of functions converges in the topology of uniform convergence if and only if it converges uniformly.
More concisely: For any filter `p` over `ι`, a sequence of functions `F` from `ι` to `UniformFun α β` converges uniformly to a function `f` of type `UniformFun α β` with respect to `p` if and only if it converges towards the neighborhood filter of `f` in the sense of `Filter.Tendsto`.
|
UniformFun.hasBasis_nhds_of_basis
theorem UniformFun.hasBasis_nhds_of_basis :
∀ (α : Type u_1) (β : Type u_2) {ι : Type u_4} [inst : UniformSpace β] (f : UniformFun α β) {p : ι → Prop}
{s : ι → Set (β × β)},
(uniformity β).HasBasis p s → (nhds f).HasBasis p fun i => {g | (f, g) ∈ UniformFun.gen α β (s i)}
This theorem, `UniformFun.hasBasis_nhds_of_basis`, states that for any given function `f` of type `α →ᵤ β`, if the uniformity filter `𝓤 β` has a basis `{s_i}` indexed by a predicate `p`, then the neighborhood filter of `f`, denoted as `𝓝 f`, has a filter basis `{g | ∀ x, (f x, g x) ∈ V}` indexed by the same predicate `p`. Here, each `V` in the basis set of `𝓝 f` consists of pairs `(f x, g x)` that belong to the corresponding basis set `s_i` of `𝓤 β`. In simpler words, the theorem connects the filter bases of the uniformity of the codomain type and the neighborhood filter of a function in the space of uniformly continuous functions.
More concisely: If `𝓤 β` is a uniformity on `β` with basis `{s_i}`, then the neighborhood filter of a function `f : α → β` has a basis `{g}` consisting of functions `g : α → β` such that `(f x, g x) ∈ s_i` for all `i` and `x`.
|
UniformFun.uniformContinuous_toFun
theorem UniformFun.uniformContinuous_toFun :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β], UniformContinuous ⇑UniformFun.toFun
The theorem `UniformFun.uniformContinuous_toFun` states that for any types `α` and `β` with `β` being a uniform space, the natural function `UniformFun.toFun` that maps from `α →ᵤ β` to `α → β` is uniformly continuous. This essentially means that, given any pair of elements in `α` that are close to each other, their images under `UniformFun.toFun` will also be close to each other. This further implies that the uniform structure of uniform convergence is more refined (i.e., has more detail) than that of pointwise convergence, also known as the product uniform structure.
More concisely: The natural function `UniformFun.toFun` from `α →ᵤ β` to `α → β` is a uniformly continuous function between uniform spaces.
|
UniformOnFun.hasBasis_nhds
theorem UniformOnFun.hasBasis_nhds :
∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖),
𝔖.Nonempty →
DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖 →
(nhds f).HasBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ uniformity β) fun SV =>
{g | (g, f) ∈ UniformOnFun.gen 𝔖 SV.1 SV.2}
This theorem states that, for a function `f : α →ᵤ[𝔖] β` where `𝔖 : Set (Set α)` is nonempty and directed, the neighborhood filter of `f` admits the family `{g | ∀ x ∈ S, (f x, g x) ∈ V}` as a basis of the filter where `S` is an element of `𝔖` and `V` is an element of the uniformity of `β`. Here, a set `𝔖` is directed if, for any two elements in the set, there's another element in the set that contains both. The basis of the filter is characterized by pairs `S` and `V` such that `S` is in `𝔖` and `V` is in the uniformity of `β`, and the basis elements are sets of functions `g` such that `(g, f)` is an element of the generator of `𝔖`-convergence with respect to `S` and `V`.
More concisely: For a function `f : α →ᵤ[𝔖] β` with nonempty and directed set `𝔖 ⊆ Set (Set α)`, the neighborhood filter of `f` has `{g | (g, f) ∈ gen_conv 𝔖 (S, V)}` as a basis for any `S ∈ 𝔖` and `V ∈ uniformity β`, where `gen_conv` denotes the generator of `𝔖`-convergence.
|
UniformFun.postcomp_uniformContinuous
theorem UniformFun.postcomp_uniformContinuous :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] [inst_1 : UniformSpace γ] {f : γ → β},
UniformContinuous f → UniformContinuous (⇑UniformFun.ofFun ∘ (fun x => f ∘ x) ∘ ⇑UniformFun.toFun)
The theorem `UniformFun.postcomp_uniformContinuous` states that if a function `f` from some type γ to another type β is uniformly continuous, then the function that post composes any function from type α to γ with `f` is also uniformly continuous. More formally, given a uniformly continuous function `f : γ → β`, the function `(fun g ↦ f ∘ g) : (α →ᵤ γ) → (α →ᵤ β)` is uniformly continuous. This means no matter where the inputs to `f` and `g` are located in their domains, as the inputs get arbitrarily close to each other, the outputs of the composed function `(f ∘ g)` also get arbitrarily close to each other.
More concisely: If `f` is a uniformly continuous function from type γ to type β, then the function `(f ∘ g)` obtained bypost composing any uniformly continuous function `g` from type α to type γ with `f` is also uniformly continuous from type α to type β.
|
UniformOnFun.mono
theorem UniformOnFun.mono :
∀ {α : Type u_1} {γ : Type u_3} ⦃u₁ u₂ : UniformSpace γ⦄,
u₁ ≤ u₂ →
∀ ⦃𝔖₁ 𝔖₂ : Set (Set α)⦄, 𝔖₂ ⊆ 𝔖₁ → UniformOnFun.uniformSpace α γ 𝔖₁ ≤ UniformOnFun.uniformSpace α γ 𝔖₂
The theorem "UniformOnFun.mono" states that for any types `α` and `γ` and for any uniform structures `u₁` and `u₂` on `γ`, if `u₁` is less than or equal to `u₂` and a set of sets `𝔖₂` is a subset of another set of sets `𝔖₁`, then the uniform space created by `𝔖₁` and `u₁` is less than or equal to the uniform space created by `𝔖₂` and `u₂`. In other words, it says that the relationship of the uniform spaces is preserved when we go from a larger uniform structure and set of sets to a smaller one.
More concisely: Given uniform structures `u₁ ≤ u₂` on type `γ` and `𝔖₁ ⊆ 𝔖₂` sets of sets, the uniform space induced by `𝔖₁` and `u₁` is less than or equal to the uniform space induced by `𝔖₂` and `u₂`.
|
UniformOnFun.gen_eq_preimage_restrict
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
This theorem states that for any set `S` of type `α` and any set `V` of type `β × β`, the generation of uniformity on functions from `α` to `β` with respect to `S` and `V` is equivalent to the preimage of the generation of uniformity on functions from `S` to `β` with respect to `V`, under the mapping that applies `S.restrict` to each component of the pair of functions. This is a key property used in proving that the family `UniformOnFun.gen S V` for each `S` in `𝔖` and `V` in the uniformity of `β`, forms a basis for the uniformity of `𝔖`-convergence, as defined in `UniformOnFun.uniformSpace`.
More concisely: The generation of uniformity on functions from a set `S` to `β` with respect to `V`, is equivalent to the preimage under `S.restrict` of the generation of uniformity on functions from `S` to `β` with respect to `V`.
|
UniformFun.iInf_eq
theorem UniformFun.iInf_eq :
∀ {α : Type u_1} {γ : Type u_3} {ι : Type u_4} {u : ι → UniformSpace γ},
UniformFun.uniformSpace α γ = ⨅ i, UniformFun.uniformSpace α γ
The theorem `UniformFun.iInf_eq` states that for any types `α`, `γ`, and `ι`, and any family `u` of uniform structures on `γ`, the uniform structure of uniform convergence `𝒰(α, γ, (⨅ i, u i))` is equal to the infimum over all `i` of the uniform structures `𝒰(α, γ, u i)`. In other words, it asserts the equality between the uniform structure of uniform convergence on the infimum of a family of uniform structures and the infimum of the uniform structures of uniform convergence on each member of the family.
More concisely: The theorem `UniformFun.iInf_eq` asserts that the uniform structure of uniform convergence on the infimum of a family of uniform structures is equal to the infimum of the uniform structures of uniform convergence on each member of the family.
|
UniformOnFun.hasBasis_uniformity_of_basis
theorem UniformOnFun.hasBasis_uniformity_of_basis :
∀ (α : Type u_1) (β : Type u_2) {ι : Type u_4} [inst : UniformSpace β] (𝔖 : Set (Set α)),
𝔖.Nonempty →
DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖 →
∀ {p : ι → Prop} {s : ι → Set (β × β)},
(uniformity β).HasBasis p s →
(uniformity (UniformOnFun α β 𝔖)).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si =>
UniformOnFun.gen 𝔖 Si.1 (s Si.2)
This theorem states that if we have a nonempty and directed set `𝔖` of subsets of `α` and `𝓑` is a filter basis of the uniformity of `β` (a uniform space), then the uniformity of the type of functions from `α` to `β` equipped with the structure of uniform convergence on `𝔖` admits a filter basis composed of the pairs of functions `(f, g)` such that for every `x` in `S` (where `S` is an element of `𝔖`), the pair `(f x, g x)` is in `V` (where `V` is an element of `𝓑`). In other words, the uniformity of these functions has a basis that reflects the uniform convergence on `𝔖` and the uniform structure of `β`.
More concisely: Given a nonempty and directed set `𝔖` of subsets of `α` and a filter basis `𝓑` of the uniformity of a uniform space `β`, the uniformity of functions from `α` to `β` with the structure of uniform convergence on `𝔖` has a filter basis consisting of pairs `(f, g)` of functions such that `(fx, gx)` is in `V` for all `V` in `𝓑` and `x` in `S` for some `S` in `𝔖`.
|
UniformOnFun.uniformContinuous_restrict
theorem UniformOnFun.uniformContinuous_restrict :
∀ (α : Type u_1) (β : Type u_2) {s : Set α} [inst : UniformSpace β] (𝔖 : Set (Set α)),
s ∈ 𝔖 → UniformContinuous (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(UniformOnFun.toFun 𝔖))
The theorem `UniformOnFun.uniformContinuous_restrict` states that for any two types `α` and `β`, a set `s` of type `α`, and a uniform space `β`, if `𝔖` is a set of sets of `α` and `s` belongs to `𝔖`, then the restriction of a function to the set `s` is a uniformly continuous function when mapping from `α →ᵤ[𝔖] β` to `↥s →ᵤ β`. The restriction operation is defined as the composition of the functions `UniformFun.ofFun`, `s.restrict`, and `UniformOnFun.toFun 𝔖`.
More concisely: For any uniform space β, if X is a uniformly continuous function from α to β and s ⊆ α belongs to a set 𝔖 of sets of α, then the restriction of X to s is uniformly continuous as a function from s to β.
|
UniformFun.inf_eq
theorem UniformFun.inf_eq :
∀ {α : Type u_1} {γ : Type u_3} {u₁ u₂ : UniformSpace γ},
UniformFun.uniformSpace α γ = UniformFun.uniformSpace α γ ⊓ UniformFun.uniformSpace α γ
The theorem `UniformFun.inf_eq` states that for any types `α` and `γ` and any two uniform structures `u₁` and `u₂` on `γ`, the uniform space of the function type from `α` to `γ` under the intersection of `u₁` and `u₂` is equal to the intersection of the uniform spaces of `α` to `γ` under `u₁` and `u₂` respectively. In other words, the uniform space of uniform convergence when the uniform structures on the codomain are intersected is the intersection of the uniform spaces when the structures are considered separately. This theorem is in the context of topology and uniform spaces.
More concisely: The uniform spaces of functions from type `α` to type `γ` under intersections of uniform structures `u₁` and `u₂` on `γ` are equal.
|
UniformFun.hasBasis_uniformity
theorem UniformFun.hasBasis_uniformity :
∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β],
(uniformity (UniformFun α β)).HasBasis (fun x => x ∈ uniformity β) (UniformFun.gen α β)
This theorem states that for any types `α` and `β`, where `β` is a uniform space, the uniformity of the function type `α →ᵤ β` has a filter basis. This filter basis is characterized by sets of pairs `(f, g)` of functions from `α` to `β`, such that for every `x` in `α`, the pair `(f x, g x)` belongs to a given set `V`. Here, `V` is drawn from the uniformity of `β`. In simpler terms, it establishes a uniform convergence structure on the space of functions from `α` to `β`, with convergence being measured with respect to the uniform structure on `β`.
More concisely: For any type `α` and uniform space `β`, the uniformity of the function type `α → β` has a filter basis characterized by sets of pairs of functions `(f, g)` such that `(fx, gx)` belongs to some set in the uniformity of `β` for all `x` in `α`.
|
UniformFun.postcomp_uniformInducing
theorem UniformFun.postcomp_uniformInducing :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] [inst_1 : UniformSpace γ] {f : γ → β},
UniformInducing f → UniformInducing (⇑UniformFun.ofFun ∘ (fun x => f ∘ x) ∘ ⇑UniformFun.toFun)
The theorem `UniformFun.postcomp_uniformInducing` states that post-composition by a uniform inducing function preserves the property of inducing a uniform structure in the context of uniform convergence. More specifically, for any types `α`, `β`, and `γ`, and given uniform spaces on `β` and `γ`, if a function `f` from `γ` to `β` is uniform inducing, then the function obtained by post-composing `f` with each function from `α` to `γ` is also uniform inducing. This new function maps from the space of uniformly continuous functions from `α` to `γ` to the space of uniformly continuous functions from `α` to `β`.
More concisely: If `f` is a uniformly inducing function from a uniform space `γ` to another uniform space `β`, then the function obtained by post-composing `f` with each uniformly continuous function from `α` to `γ` is a uniformly inducing function from the space of uniformly continuous functions from `α` to `γ` to the space of uniformly continuous functions from `α` to `β`.
|
UniformFun.gc
theorem UniformFun.gc :
∀ (α : Type u_1) (β : Type u_2),
GaloisConnection (fun 𝓐 => Filter.map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α β 𝓕
The theorem `UniformFun.gc` states that for any types `α` and `β`, there exists a Galois connection between two functions. A Galois connection is a pair of functions `l` and `u` such that for all `a` and `b`, `l a ≤ b` is equivalent to `a ≤ u b`. In this case, the functions are `fun 𝓐 => Filter.map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)` and `fun 𝓕 => UniformFun.filter α β 𝓕`. The function `Filter.map` maps a filter through a function. The function `UniformFun.filter` generates a filter from a filter on pairs of `β` to a filter on pairs of uniform functions from `α` to `β`. The theorem does not specify the exact definition of the lower adjoint `l`, but assures its existence and states that it has certain properties.
More concisely: For any types α and β, there exists a Galois connection between the functions `Filter.map (UniformFun.phi α β) (· ×⊤)` and `UniformFun.filter α β`.
|
UniformOnFun.comap_eq
theorem UniformOnFun.comap_eq :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {𝔖 : Set (Set α)} {f : γ → β},
UniformOnFun.uniformSpace α γ 𝔖 = UniformSpace.comap (fun x => f ∘ x) (UniformOnFun.uniformSpace α β 𝔖)
The theorem `UniformOnFun.comap_eq` states that for any types `α`, `β`, and `γ`, a uniform space structure `inst` on `β`, a set `𝔖` of subsets of `α`, and a function `f` from `γ` to `β`, the uniform structure on functions from `α` to `γ` induced by `𝔖` is the same as the uniform structure obtained by taking the preimage under the function composition `f ∘ x` of the uniform structure on functions from `α` to `β` induced by `𝔖`. In simpler terms, this theorem expresses an equality between two ways of constructing a uniform structure on the function space from `α` to `γ`, either directly or by precomposing with a given function `f`.
More concisely: For any uniform spaces (β, inst) on type β, set 𝔖 of subsets of α, and function f from γ to β, the uniform structure on Functions from α to γ induced by 𝔖 is equal to the preimage under f ∘ x of the uniform structure on Functions from α to β induced by 𝔖.
|
UniformOnFun.uniformContinuous_eval_of_mem
theorem UniformOnFun.uniformContinuous_eval_of_mem :
∀ {α : Type u_1} (β : Type u_2) {s : Set α} [inst : UniformSpace β] (𝔖 : Set (Set α)) {x : α},
x ∈ s → s ∈ 𝔖 → UniformContinuous (Function.eval x ∘ ⇑(UniformOnFun.toFun 𝔖))
The theorem `UniformOnFun.uniformContinuous_eval_of_mem` states that, for any type `α`, another type `β` with a uniform space structure, a set `s` of `α` type, a collection `𝔖` of sets of `α`, and an element `x` of `α`, if `x` belongs to `s` and `s` is a member of the set collection `𝔖`, then the function that evaluates at `x` when composed with the function that reinterprets `α →ᵤ[𝔖] β` as an element of `α → β` is uniformly continuous. In other words, when we pick a certain `x` from a set `s` in the collection `𝔖`, the evaluation function at `x` will always map close points to close points, regardless of their location in `α`, when considering the reinterpreted function from `α` to `β`.
More concisely: For any type `α`, uniform space `β`, set `s ���itzerland α` in a collection `𝔖`, and `x ∈ s`, the evaluation function `λ (a : α). ( eval (a : α →ᵤ[𝔖] β) x ) : β` is uniformly continuous.
|
UniformOnFun.postcomp_uniformContinuous
theorem UniformOnFun.postcomp_uniformContinuous :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace β] {𝔖 : Set (Set α)} [inst_1 : UniformSpace γ]
{f : γ → β},
UniformContinuous f → UniformContinuous (⇑(UniformOnFun.ofFun 𝔖) ∘ (fun x => f ∘ x) ∘ ⇑(UniformOnFun.toFun 𝔖))
This theorem states that post-composing a function by a uniformly continuous function results in a uniformly continuous function, under a uniform structure of set-convergence. More specifically, given a uniformly continuous function `f` from `γ` to `β`, the operation `(fun g ↦ f ∘ g)` that post-composes any function `g` from `α` to `γ` with `f` produces a uniformly continuous function from `α` to `β`. This holds true for any uniform spaces `β` and `γ`, and any set `𝔖` of sets of `α`.
More concisely: Given uniform spaces `β` and `γ`, and a uniformly continuous function `f` from `γ` to `β`, the function `(fun g ↦ f ∘ g)` is uniformly continuous from `α` to `β` for any set `𝔖` of sets of `α`.
|
UniformFun.hasBasis_nhds
theorem UniformFun.hasBasis_nhds :
∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β] (f : UniformFun α β),
(nhds f).HasBasis (fun V => V ∈ uniformity β) fun V => {g | (f, g) ∈ UniformFun.gen α β V}
The theorem named `UniformFun.hasBasis_nhds` states that for every uniform space `β` and every function `f` from one type `α` to `β`, the neighborhood filter of `f` (denoted by `𝓝 f`) is generated by a basis consisting of sets of the form `{g | ∀ x, (f x, g x) ∈ V}`, where `V` is drawn from the uniformity of `β` (denoted by `𝓤 β`). In other words, these sets form a filter basis for the neighborhood filter of `f`, capturing the idea that `f` and `g` are "close" if their values are "close" for every input.
More concisely: The neighborhood filter of a function from type `α` to uniform space `β` is generated by sets of the form `{g : β | ∀ x : α, (f x, g x) ∈ V}`, where `V` is from the uniformity of `β`.
|
UniformFun.mono
theorem UniformFun.mono : ∀ {α : Type u_1} {γ : Type u_3}, Monotone (@UniformFun.uniformSpace α γ)
The theorem `UniformFun.mono` states that if you have two uniform structures `u₁` and `u₂` on a type `γ`, and `u₁` is lesser than or equal to `u₂` (in the sense that `u₁` is a sub-uniform structure of `u₂`), then the uniform space associated with `α` and `γ` with respect to `u₁` is also lesser than or equal to the uniform space associated with `α` and `γ` with respect to `u₂`. In other words, the function mapping a uniform structure on `γ` to the corresponding uniform structure of uniform convergence on functions from `α` to `γ` is monotone.
More concisely: If `u₁` is a sub-uniform structure of `u₂` on type `γ`, then the uniform structure of uniform convergence on functions from `α` to `γ` induced by `u₁` is less or equal to the one induced by `u₂`.
|