uniformEquicontinuousOn_iff_uniformContinuousOn
theorem uniformEquicontinuousOn_iff_uniformContinuousOn :
∀ {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : UniformSpace α] [uβ : UniformSpace β] {F : ι → β → α}
{S : Set β}, UniformEquicontinuousOn F S ↔ UniformContinuousOn (⇑UniformFun.ofFun ∘ Function.swap F) S
The theorem states that for a family of functions `𝓕 : ι → β → α`, it is uniformly equicontinuous on a set `S` if and only if the function `swap 𝓕 : β → ι → α` is uniformly continuous on `S` when the function type `ι → α` is equipped with the uniform structure of uniform convergence. In simpler terms, this theorem connects the concept of uniform equicontinuity of a family of functions to the uniform continuity of a function obtained by swapping the arguments of the original function. This is primarily used for developing the equicontinuity application programming interface (API) and is not intended for direct use in other contexts.
More concisely: A family of functions `𝓕 : ι → β → α` is uniformly equicontinuous on a set `S` if and only if the swapped function `swap 𝓕 : β → ι → α` is uniformly continuous on `S` with respect to the uniform structure of uniform convergence on `ι → α`.
|
UniformEquicontinuous.closure'
theorem UniformEquicontinuous.closure' :
∀ {Y : Type u_5} {α : Type u_7} {β : Type u_9} [tY : TopologicalSpace Y] [uα : UniformSpace α] [uβ : UniformSpace β]
{A : Set Y} {u : Y → β → α},
UniformEquicontinuous (u ∘ Subtype.val) → Continuous u → UniformEquicontinuous (u ∘ Subtype.val)
The theorem `UniformEquicontinuous.closure'` states that if a set of functions is uniformly equicontinuous, then its closure remains uniformly equicontinuous in any topology, given that the evaluation at any point is continuous. This theorem is applicable to any topological space with a mapping to function space `β → α` that satisfies the appropriate continuity conditions. This theorem will primarily be applied to `DFunLike` types, but it also generalizes the concept of the closure of uniformly equicontinuous functions for any set.
More concisely: If a set of continuous functions from a topological space to another is uniformly equicontinuous, then its closure is also uniformly equicontinuous in any topology.
|
Equicontinuous.closure'
theorem Equicontinuous.closure' :
∀ {X : Type u_3} {Y : Type u_5} {α : Type u_7} [tX : TopologicalSpace X] [tY : TopologicalSpace Y]
[uα : UniformSpace α] {A : Set Y} {u : Y → X → α},
Equicontinuous (u ∘ Subtype.val) → Continuous u → Equicontinuous (u ∘ Subtype.val)
The theorem `Equicontinuous.closure'` states that for any types `X`, `Y`, and `α` with `X` and `Y` being topological spaces and `α` being a uniform space, given a set `A` of `Y` and a function `u` from `Y` to `X → α`, if the composition of `u` and the underlying element of the subtype is equicontinuous, and `u` is continuous, then the composition of `u` and the underlying element of the subtype remains equicontinuous. This theorem generalizes the concept of equicontinuity of a set of functions to its closure in any topology where evaluation at any point continues to be continuous. It's mainly applicable to `DFunLike` types that satisfy the right continuity conditions.
More concisely: If a set of functions from a topological space to another and a uniform space `α`, where evaluation at every point is continuous, is equicontinuous and each function is continuous, then the closure of this set in any topology preserves equicontinuity.
|
equicontinuousAt_iff_range
theorem equicontinuousAt_iff_range :
∀ {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α}
{x₀ : X}, EquicontinuousAt F x₀ ↔ EquicontinuousAt Subtype.val x₀
The theorem `equicontinuousAt_iff_range` states that a family of functions `𝓕 : ι → X → α`, where `X` is a topological space and `α` is a uniform space, is equicontinuous at a point `x₀` if and only if the range of that family, as indicated by `(↑) : range F → X → α`, is equicontinuous at `x₀`. In other words, the equicontinuity of the function family at a point depends solely on the equicontinuity of its range at that same point.
More concisely: A family of functions from a topological space to a uniform space is equicontinuous at a point if and only if its range is equicontinuous at that point.
|
UniformInducing.uniformEquicontinuous_iff
theorem UniformInducing.uniformEquicontinuous_iff :
∀ {ι : Type u_1} {α : Type u_7} {β : Type u_9} {γ : Type u_11} [uα : UniformSpace α] [uβ : UniformSpace β]
[uγ : UniformSpace γ] {F : ι → β → α} {u : α → γ},
UniformInducing u → (UniformEquicontinuous F ↔ UniformEquicontinuous ((fun x => u ∘ x) ∘ F))
The theorem states that, given a map `u` from `α` to `γ` that induces a uniform structure on `α`, a family of functions `𝓕` from `ι` to `β → α` is uniformly equicontinuous if and only if the family `𝓕'`, which is obtained by composing each function of `𝓕` with `u`, is also uniformly equicontinuous. In other words, if for every function in the family `𝓕`, the composition of that function with `u` is uniformly equicontinuous, then `𝓕` itself must be uniformly equicontinuous, and vice versa. This establishes a correspondence between the uniform equicontinuity of a family of functions and the uniform equicontinuity of their compositions with a uniform inducing map.
More concisely: Given a uniformly continuous map `u : α → γ` inducing a uniform structure on `α`, a family `𝓕 : ι → β → α` is uniformly equicontinuous if and only if the family `𝓕' : ι → β → γ` obtained by composing each function in `𝓕` with `u` is also uniformly equicontinuous.
|
EquicontinuousAt.closure'
theorem EquicontinuousAt.closure' :
∀ {X : Type u_3} {Y : Type u_5} {α : Type u_7} [tX : TopologicalSpace X] [tY : TopologicalSpace Y]
[uα : UniformSpace α] {A : Set Y} {u : Y → X → α} {x₀ : X},
EquicontinuousAt (u ∘ Subtype.val) x₀ → Continuous u → EquicontinuousAt (u ∘ Subtype.val) x₀
The theorem `EquicontinuousAt.closure'` states the following:
If a set of functions is equicontinuous at some point `x₀`, then the same property holds for its closure in any topology, given that the evaluation at any point is continuous. This is true for any topological space with a map to `X → α` satisfying the right continuity conditions. This theorem is particularly applied to `DFunLike` types. The theorem specifically states that for any types `X`, `Y`, `α`, any topological spaces `tX` and `tY`, any uniform space `uα`, any set `A` of `Y`, any function `u` from `Y` to `X` to `α`, and any `x₀` in `X`, if `u ∘ Subtype.val` is equicontinuous at `x₀` and `u` is continuous, then `u ∘ Subtype.val` is equicontinuous at `x₀` in the closure.
More concisely: If a set of functions is equicontinuous at a point in a topological space and the functions are continuous, then the set of functions is equicontinuous at that point in the closure of the domain in any topology satisfying the right continuity conditions.
|
EquicontinuousAt.continuousAt
theorem EquicontinuousAt.continuousAt :
∀ {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α}
{x₀ : X}, EquicontinuousAt F x₀ → ∀ (i : ι), ContinuousAt (F i) x₀
The theorem `EquicontinuousAt.continuousAt` states that for any family of functions `F` mapping from a topological space `X` to a uniform space `α`, if the family `F` is equicontinuous at a point `x₀` from `X`, then every function in the family `F` is continuous at that point `x₀`. In other words, equicontinuity of a family of functions at a point implies the continuity of each function in that family at the same point.
More concisely: If a family of functions from a topological space to a uniform space is equicontinuous at a point, then each function in the family is continuous at that point.
|
UniformInducing.equicontinuousAt_iff
theorem UniformInducing.equicontinuousAt_iff :
∀ {ι : Type u_1} {X : Type u_3} {α : Type u_7} {β : Type u_9} [tX : TopologicalSpace X] [uα : UniformSpace α]
[uβ : UniformSpace β] {F : ι → X → α} {x₀ : X} {u : α → β},
UniformInducing u → (EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x => u ∘ x) ∘ F) x₀)
The theorem states that given a mapping `u` from a set `α` to `β` that induces a uniform structure, a family `𝓕` of functions from a topological space `X` to the uniform space `α` is equicontinuous at a point `x₀` in `X` if and only if the family `𝓕'` of functions, obtained by composing each function in `𝓕` with `u`, is also equicontinuous at `x₀`. In other words, the uniformity inducing property of `u` preserves the equicontinuity of the family of functions at a particular point.
More concisely: Given a uniformly continuous map `u : α → β` and a family `𝓕` of equicontinuous functions `f : X → α` at `x₀ ∈ X`, the composition `g ∘ u` of each `g ∈ 𝓕` with `u` is also an equicontinuous family of functions at `x₀`.
|
EquicontinuousAt.tendsto_of_mem_closure
theorem EquicontinuousAt.tendsto_of_mem_closure :
∀ {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : TopologicalSpace X] [uα : UniformSpace α] {l : Filter ι}
{F : ι → X → α} {f : X → α} {s : Set X} {x : X} {z : α},
EquicontinuousAt F x →
Filter.Tendsto f (nhdsWithin x s) (nhds z) →
(∀ y ∈ s, Filter.Tendsto (fun x => F x y) l (nhds (f y))) →
x ∈ closure s → Filter.Tendsto (fun x_1 => F x_1 x) l (nhds z)
The theorem `EquicontinuousAt.tendsto_of_mem_closure` states that given a family of functions `F` from a topological space `X` to a uniform space `α` that is equicontinuous at a point `x`, a set `s` in `X`, a limit function `f : X → α`, a filter `l` on `ι`, and a point `z` in `α` such that every function in the family `F` tends to `f(y)` along the filter `l` for any `y` in `s`, the limit function `f` tends to `z` along the neighborhood filter of `x` within `s`, and `x` is in the closure of `s`, then the function `F` composed with `x` tends to `z` along the filter `l`. In other words, if the functions in the family `F` are equicontinuous at `x` and tend consistently to the values of the limit function `f` within the set `s`, and `f` itself tends towards a specific value `z` within the neighborhood of `x` in `s`, then we can expect the function value at `x` to tend towards `z` when `x` is a limit point of `s`.
More concisely: Given an equicontinuous family of functions from a topological space to a uniform space, if every function in the family tends to a limit function at a point in the closure of a set and the limit function tends to a value at that point, then the composition of the family with the point tends to that value along the filter of neighborhoods of the point within the set.
|
EquicontinuousAt.comp
theorem EquicontinuousAt.comp :
∀ {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_7} [tX : TopologicalSpace X] [uα : UniformSpace α]
{F : ι → X → α} {x₀ : X}, EquicontinuousAt F x₀ → ∀ (u : κ → ι), EquicontinuousAt (F ∘ u) x₀
The theorem "EquicontinuousAt.comp" states that if a family `F` of functions from a topological space `X` to a uniform space `α` is equicontinuous at a point `x₀`, then for any function `u` mapping from some type `κ` to the index set `ι`, the sub-family of `F` composed with `u` is also equicontinuous at the same point `x₀`. In other words, equicontinuity at a point is preserved when taking sub-families of the function family `F`.
More concisely: If a family of functions from a topological space to a uniform space is equicontinuous at a point, then any sub-family composed with a function mapping to the index set is also equicontinuous at that point.
|
Equicontinuous.continuous
theorem Equicontinuous.continuous :
∀ {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α},
Equicontinuous F → ∀ (i : ι), Continuous (F i)
The theorem states that for any equicontinuous family of functions `F` mapping points from a topological space `X` to a uniform space `α`, each individual function within this family is continuous. Here, `Equicontinuous F` means that the family `F` is equicontinuous on all of `X`, i.e., it is equicontinuous at each point of `X`. The theorem guarantees that for any function selected from this family (indexed by `i`), that function is a continuous function.
More concisely: Every function in an equicontinuous family mapping points from a topological space to a uniform space is continuous.
|
UniformEquicontinuous.uniformContinuous
theorem UniformEquicontinuous.uniformContinuous :
∀ {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : UniformSpace α] [uβ : UniformSpace β] {F : ι → β → α},
UniformEquicontinuous F → ∀ (i : ι), UniformContinuous (F i)
This theorem states that every function within a uniformly equicontinuous family of functions is uniformly continuous. In other words, given a uniformly equicontinuous family `F` of functions from a uniform space `β` to another uniform space `α`, each individual function `F i` (for any `i` in the indexing set `ι`) is uniformly continuous. This implies that if points in `β` are sufficiently close to each other, their images under any function from the family will also be close to each other, regardless of where the points are located in `β`.
More concisely: If `F` is a uniformly equicontinuous family of functions from the uniform space `β` to the uniform space `α`, then each function `F i` in `F` is uniformly continuous.
|
EquicontinuousWithinAt.closure'
theorem EquicontinuousWithinAt.closure' :
∀ {X : Type u_3} {Y : Type u_5} {α : Type u_7} [tX : TopologicalSpace X] [tY : TopologicalSpace Y]
[uα : UniformSpace α] {A : Set Y} {u : Y → X → α} {S : Set X} {x₀ : X},
EquicontinuousWithinAt (u ∘ Subtype.val) S x₀ →
Continuous (S.restrict ∘ u) →
Continuous (Function.eval x₀ ∘ u) → EquicontinuousWithinAt (u ∘ Subtype.val) S x₀
The theorem `EquicontinuousWithinAt.closure'` states that for any types `X`, `Y`, and `α`, given a topological space over `X` and `Y`, a uniform space over `α`, a set `A` of type `Y`, a function `u` from `Y` to the function type `X → α`, a set `S` of type `X`, and an element `x₀` of type `X`, if the function `u` composed with `Subtype.val` is equicontinuous within `S` at `x₀`, and the function `Set.restrict S` composed with `u`, as well as `Function.eval x₀` composed with `u` are continuous, then the function `u` composed with `Subtype.val` remains equicontinuous within `S` at `x₀` for the closure of the set of functions in any topology, provided the evaluation at any `x` in the union of sets `S` and `{x₀}` is continuous.
More concisely: If a function from a set to a uniform space is equicontinuous within a subset at a point, is continuous when restricted to the subset and at the point, and the evaluation at any point in the union of the subset and the point is continuous, then the function remains equicontinuous within the subset at the point for the closure of the set of functions in any topology.
|
equicontinuous_iff_range
theorem equicontinuous_iff_range :
∀ {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α},
Equicontinuous F ↔ Equicontinuous Subtype.val
The theorem `equicontinuous_iff_range` asserts that a family of functions `𝓕 : ι → X → α`, mapping a topological space `X` to a uniform space `α`, is equicontinuous if and only if `range 𝓕` is equicontinuous. In other words, the family of functions `(↑) : range F → X → α` is equicontinuous. Here, equicontinuous means that the family `𝓕` is equicontinuous at each point of `X`, and `range 𝓕` denotes the image of the family `𝓕` under the map, with each underlying element in the base type accessed via the Subtype.val function.
More concisely: A family of functions from a topological space to a uniform space is equicontinuous if and only if its range is equicontinuous.
|
UniformInducing.equicontinuous_iff
theorem UniformInducing.equicontinuous_iff :
∀ {ι : Type u_1} {X : Type u_3} {α : Type u_7} {β : Type u_9} [tX : TopologicalSpace X] [uα : UniformSpace α]
[uβ : UniformSpace β] {F : ι → X → α} {u : α → β},
UniformInducing u → (Equicontinuous F ↔ Equicontinuous ((fun x => u ∘ x) ∘ F))
The theorem states that if we have a map `u` that induces a uniform structure from a set `α` to a set `β`, then a family of functions `𝓕` mapping from a topological space `X` to `α` is equicontinuous if and only if the family `𝓕'`, which is obtained by composing each function in `𝓕` with `u`, is also equicontinuous. In simpler terms, applying a uniform inducing map to each function in an equicontinuous family of functions preserves the equicontinuity property.
More concisely: If `u : α → β` is a uniformly continuous map inducing a uniform structure on `α`, then the family of functions `{f : X → α | f ∣ X ↪ α is continuous}` is equicontinuous if and only if the family `{u ∘ f | f ∈ {f : X → α | f ∣ X ↪ α is continuous}}` is equicontinuous.
|
equicontinuousWithinAt_iff_continuousWithinAt
theorem equicontinuousWithinAt_iff_continuousWithinAt :
∀ {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α}
{S : Set X} {x₀ : X},
EquicontinuousWithinAt F S x₀ ↔ ContinuousWithinAt (⇑UniformFun.ofFun ∘ Function.swap F) S x₀
The theorem `equicontinuousWithinAt_iff_continuousWithinAt` states that for a family of functions `F : ι → X → α` (indexed by ι), it is equicontinuous at a point `x₀` within a set `S` if and only if the function `swap 𝓕 : X → ι → α` (which swaps the order of arguments) is continuous at `x₀` within `S`, where the function space `ι → α` is equipped with the topology of uniform convergence. This result is particularly useful in developing the equicontinuity API, but it's recommended not to use it directly for other purposes. Note that the topological space structure is on `X` and the uniform space structure is on `α`.
More concisely: A family of functions \(F : ι → X → α\) is equicontinuous at a point \(x\_0 ∈ S \subseteq X\) if and only if the function \(swap 𝓕 : X → ι → α\) is continuous at \(x\_0\) within \(S\) with respect to the uniform convergence topology on \(ι → α\).
|
Mathlib.Topology.UniformSpace.Equicontinuity._auxLemma.19
theorem Mathlib.Topology.UniformSpace.Equicontinuity._auxLemma.19 :
∀ {α : Type u_1} {β : Type u_2} {p : α × β → Prop}, (∀ (x : α × β), p x) = ∀ (a : α) (b : β), p (a, b)
This theorem states that for any property `p` which applies to pairs of elements from types `α` and `β`, stating that this property holds for all pairs `(x : α × β)` is equivalent to stating that the property holds for all possible pairs constructed as `(a : α) (b : β)`. In other words, the property applies to all individual combinations of elements from `α` and `β`.
More concisely: The theorem asserts that a property `p` defined on pairs from types `α × β` is equivalent to the same property on individual elements `(a : α) (b : β)`.
|
Equicontinuous.comp
theorem Equicontinuous.comp :
∀ {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_7} [tX : TopologicalSpace X] [uα : UniformSpace α]
{F : ι → X → α}, Equicontinuous F → ∀ (u : κ → ι), Equicontinuous (F ∘ u)
The theorem `Equicontinuous.comp` states that taking sub-families preserves equicontinuity. This means for any types `ι`, `κ`, `X`, and `α`, where `X` is a topological space and `α` is a uniform space, if we have a family of functions `F` from `X` to `α` indexed by `ι` that is equicontinuous, then for any function `u` from `κ` to `ι`, the composition of `F` and `u`, which gives a sub-family of `F`, is also equicontinuous. In other words, if `F` is equicontinuous at every point in `X`, then so is the sub-family `(F ∘ u)`.
More concisely: If `F: X → α` is equicontinuous and `u: κ → ι` is any function, then the composite function `F ∘ u: κ → α` is also equicontinuous.
|
equicontinuous_iff_continuous
theorem equicontinuous_iff_continuous :
∀ {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α},
Equicontinuous F ↔ Continuous (⇑UniformFun.ofFun ∘ Function.swap F)
The theorem `equicontinuous_iff_continuous` states that a family of functions `𝓕 : ι → X → α` is equicontinuous (i.e., it is equicontinuous at each point of `X`) if and only if the function obtained by swapping the arguments of `𝓕` (so it becomes `X → ι → α`) is continuous, when `ι → α` is equipped with the topology of uniform convergence. This concept is particularly beneficial when developing the equicontinuity API, although it is not intended to be used directly for other applications.
More concisely: A family of functions is equicontinuous if and only if the function obtained by swapping arguments is continuous with respect to uniform convergence of functions.
|
equicontinuousWithinAt_univ
theorem equicontinuousWithinAt_univ :
∀ {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : TopologicalSpace X] [uα : UniformSpace α] (F : ι → X → α)
(x₀ : X), EquicontinuousWithinAt F Set.univ x₀ ↔ EquicontinuousAt F x₀
The theorem `equicontinuousWithinAt_univ` states that for any type `ι`, a topological space `X`, a uniform space `α`, and a family `F` of functions from `X` to `α`, the family `F` is equicontinuous within the universal set at a point `x₀` if and only if it is equicontinuous at `x₀`. In mathematical terms, for all entourages `U` in the uniform space `α`, there is a neighborhood `V` of `x₀` such that for all `x` in `V` and for all `i` in `ι`, the value `F i x` is `U`-close to `F i x₀`.
More concisely: A family of functions from a topological space to a uniform space is equicontinuous within the universal set at a point if and only if it is equicontinuous at that point. That is, for every entourage in the uniform space, there exists a neighborhood of the point such that for all functions in the family and points in the neighborhood, the values of the functions are close to the values at the point.
|
UniformEquicontinuous.comp
theorem UniformEquicontinuous.comp :
∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_7} {β : Type u_9} [uα : UniformSpace α] [uβ : UniformSpace β]
{F : ι → β → α}, UniformEquicontinuous F → ∀ (u : κ → ι), UniformEquicontinuous (F ∘ u)
The theorem `UniformEquicontinuous.comp` states that if we have a uniformly equicontinuous family of functions from a type `ι` to a uniform space `β → α`, then taking a sub-family of those functions (denoted by `u : κ → ι`) preserves the property of uniform equicontinuity. In other words, if `F` is uniformly equicontinuous, then the composition `F ∘ u` (which represents a sub-family of `F`) is also uniformly equicontinuous. In mathematical terms, for all entourages `U` in the uniform space `α`, there exists an entourage `V` in the uniform space `β` such that, for any two `V`-close points `x` and `y` in `β`, for all indices `i` in `κ`, `F(u(i)) x` is `U`-close to `F(u(i)) y`.
More concisely: If `F: ι → β → α` is uniformly equicontinuous and `u : κ → ι` is a function, then `F ∘ u: κ → α` is also uniformly equicontinuous.
|
equicontinuousAt_iff_pair
theorem equicontinuousAt_iff_pair :
∀ {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α}
{x₀ : X},
EquicontinuousAt F x₀ ↔ ∀ U ∈ uniformity α, ∃ V ∈ nhds x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
This theorem provides an alternative formulation of equicontinuity at a point `x₀`. A family of functions `F` from a topological space to a uniform space is equicontinuous at `x₀` if and only if, for every entourage `U` in the uniformity of the target space, there exists a neighborhood `V` of `x₀` such that, for any two points `x` and `y` in `V`, and for all indices `i`, the pair `(F i x, F i y)` is in `U`. This contrasts with the original definition, which only compares the function values at `x` and `x₀` for a single point `x` near `x₀`.
More concisely: A family of functions from a topological space to a uniform space is equicontinuous at a point if and only if for every entourage in the uniformity of the target space, there exists a neighborhood of the point such that any two points in the neighborhood map to each other under each function within the entourage.
|
equicontinuousAt_iff_continuousAt
theorem equicontinuousAt_iff_continuousAt :
∀ {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α}
{x₀ : X}, EquicontinuousAt F x₀ ↔ ContinuousAt (⇑UniformFun.ofFun ∘ Function.swap F) x₀
The theorem `equicontinuousAt_iff_continuousAt` states that a family of functions `𝓕 : ι → X → α`, mapping from a topological space to a uniform space, is equicontinuous at a point `x₀` if and only if the function obtained by swapping the arguments of `𝓕` (i.e., `swap 𝓕 : X → ι → α`) is continuous at `x₀` when we equip `ι → α` with the topology of uniform convergence. This theorem is particularly useful for developing the equicontinuity API, but it's recommended not to use it directly for other purposes.
More concisely: A family of functions from a topological space to a uniform space is equicontinuous at a point if and only if the function obtained by swapping arguments is continuous at that point with respect to uniform convergence.
|
Equicontinuous.isClosed_setOf_tendsto
theorem Equicontinuous.isClosed_setOf_tendsto :
∀ {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : TopologicalSpace X] [uα : UniformSpace α] {l : Filter ι}
{F : ι → X → α} {f : X → α},
Equicontinuous F → Continuous f → IsClosed {x | Filter.Tendsto (fun x_1 => F x_1 x) l (nhds (f x))}
The theorem `Equicontinuous.isClosed_setOf_tendsto` states that if we have a family of functions `F : ι → X → α` which is equicontinuous (meaning it is equicontinuous at every point in the topological space `X`), a continuous function `f : X → α`, and a filter `l` on `ι`, then the set of all `x` for which the function `F` tends to the neighborhood of `f(x)` under the filter `l` is a closed set.
In more mathematical terms, given a filter `l` and two function families `F : ι → X → α` (which is equicontinuous) and `f : X → α` (which is continuous), the set `{x | Filter.Tendsto (fun x_1 => F x_1 x) l (nhds (f x))}` is closed. Here, `Filter.Tendsto (fun x_1 => F x_1 x) l (nhds (f x))` is saying that for each neighborhood of `f(x)`, the preimage under `F` is a neighborhood under the filter `l`. In this context, a set is said to be 'closed' if its complement is open.
More concisely: Given an equicontinuous family of functions `F : ι → X → α` and a continuous function `f : X → α`, the set of points `x` in `X` such that the sequence `(F x i)` tends to `f(x)` for every net `i` in the filter `l` forms a closed subset of `X`.
|
Filter.Tendsto.uniformContinuous_of_uniformEquicontinuous
theorem Filter.Tendsto.uniformContinuous_of_uniformEquicontinuous :
∀ {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : UniformSpace α] [uβ : UniformSpace β] {l : Filter ι}
[inst : l.NeBot] {F : ι → β → α} {f : β → α},
Filter.Tendsto F l (nhds f) → UniformEquicontinuous F → UniformContinuous f
This theorem states that if a family of functions `𝓕 : ι → β → α` converges pointwise to a function `f : β → α` along some non-empty filter, and if this family of functions is uniformly equicontinuous, then the limit function `f` is uniformly continuous. In other words, if each function in the family changes continuously and uniformly across its domain and converges to a limit function under a given non-empty filter, then this limit function is also uniformly continuous. This means that, no matter where in the domain, the limit function's values are close together when the inputs are close together.
More concisely: If a pointwise convergent and uniformly equicontinuous family of functions from a filter to a space has a limit function, then that function is uniformly continuous.
|
UniformEquicontinuous.equicontinuous
theorem UniformEquicontinuous.equicontinuous :
∀ {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : UniformSpace α] [uβ : UniformSpace β] {F : ι → β → α},
UniformEquicontinuous F → Equicontinuous F
The theorem `UniformEquicontinuous.equicontinuous` asserts that for any family `F : ι → β → α` of functions between uniform spaces `α` and `β`, if the family `F` is uniformly equicontinuous, then it is equicontinuous. In other words, if for any entourage `U` in the uniformity of `α`, there exists an entourage `V` in the uniformity of `β` such that for every `V`-close pair of points `x` and `y`, all functions `F i` map `x` and `y` into `U`-close points in `α`, then `F` is equicontinuous, i.e., it is equicontinuous at each point of the domain `β`.
More concisely: If a family of functions between uniform spaces is uniformly equicontinuous, then it is equicontinuous.
|
Filter.Tendsto.continuousAt_of_equicontinuousAt
theorem Filter.Tendsto.continuousAt_of_equicontinuousAt :
∀ {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : TopologicalSpace X] [uα : UniformSpace α] {l : Filter ι}
[inst : l.NeBot] {F : ι → X → α} {f : X → α} {x₀ : X},
Filter.Tendsto F l (nhds f) → EquicontinuousAt F x₀ → ContinuousAt f x₀
The theorem states: If a family of functions `𝓕 : ι → X → α` converges pointwise to a function `f : X → α` with respect to a nontrivial filter, and if the family `𝓕` is equicontinuous at a point `x₀ : X`, then the limit function `f` is continuous at the point `x₀`. Here, "equicontinuous at a point" means that for any given distance in the output space, there exists a neighborhood around the point in the input space such that all the functions in the family map points from that neighborhood to within the given distance of the output for the original point.
More concisely: If a pointwise convergent and equicontinuous family of functions from a filter converges to a limit function at a point, then the limit function is continuous at that point.
|
uniformEquicontinuous_iff_uniformContinuous
theorem uniformEquicontinuous_iff_uniformContinuous :
∀ {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : UniformSpace α] [uβ : UniformSpace β] {F : ι → β → α},
UniformEquicontinuous F ↔ UniformContinuous (⇑UniformFun.ofFun ∘ Function.swap F)
The theorem `uniformEquicontinuous_iff_uniformContinuous` states that a family of functions `𝓕`, mapping from a type `ι` to a function from `β` to `α`, is uniformly equicontinuous if and only if the function obtained by swapping the arguments of `𝓕` (thus mapping from `β` to a function from `ι` to `α`) is uniformly continuous when `ι → α` is equipped with the uniform structure of uniform convergence. This theorem is useful for developing the equicontinuity API in Lean, but it is not recommended to use it directly for other purposes. Here, uniform equicontinuity means that given any entourage (a certain kind of set) `U` in the uniformity of `α`, there exists an entourage `V` in the uniformity of `β` such that if `x` and `y` are `V`-close, then for all `i` in `ι`, `𝓕 i x` is `U`-close to `𝓕 i y`. Uniform continuity of a function `f` from `α` to `β` requires that `(f x, f y)` tends to the diagonal as `(x, y)` tends to the diagonal, i.e., if `x` is sufficiently close to `y`, then `f x` is close to `f y` no matter where `x` and `y` are located in `α`.
More concisely: A family of functions from a type to functions from another type is uniformly equicontinuous if and only if the function obtained by swapping the arguments is uniformly continuous in the uniform structure of uniform convergence.
|