ContinuousMap.tendsto_of_tendstoLocallyUniformly
theorem ContinuousMap.tendsto_of_tendstoLocallyUniformly :
∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {f : C(α, β)} {ι : Type u₃}
{p : Filter ι} {F : ι → C(α, β)},
TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p → Filter.Tendsto F p (nhds f)
The theorem `ContinuousMap.tendsto_of_tendstoLocallyUniformly` states that for all types `α` and `β`, where `α` has a topological space structure and `β` has a uniform space structure, given a continuous map `f` from `α` to `β`, an index set `ι`, a filter `p` on `ι`, and a sequence of continuous maps `F` from `ι` to the continuous maps from `α` to `β`, if the sequence of functions `F` converges locally uniformly to the limiting function `f` with respect to the filter `p` (in other words, for every entourage of the diagonal in `β`, and for every element `x` in `α`, there exists a neighborhood of `x` such that for all `y` in this neighborhood, the values of `f(y)` and `F(n)(y)` for `p`-almost every `n` are within the entourage), then the sequence `F` tends to `f` with respect to the filter `p` and the neighborhood filter at `f` in the compact-open topology. In mathematical terms, if for every neighborhood of the diagonal, and for every point, there is a neighborhood of this point such that the sequence of function values at every point in this neighborhood is eventually within this neighborhood of the diagonal, then the sequence of functions converges to the limit function in the compact-open topology.
More concisely: Given a continuous map from a topological space to a uniform space, if the sequence of continuous maps converges locally uniformly to the limit function with respect to a filter, then the sequence tends to the limit function in the compact-open topology.
|
ContinuousMap.tendsto_iff_tendstoUniformly
theorem ContinuousMap.tendsto_iff_tendstoUniformly :
∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {f : C(α, β)} {ι : Type u₃}
{p : Filter ι} {F : ι → C(α, β)} [inst_2 : CompactSpace α],
Filter.Tendsto F p (nhds f) ↔ TendstoUniformly (fun i a => (F i) a) (⇑f) p
The theorem `ContinuousMap.tendsto_iff_tendstoUniformly` states that for any types `α` and `β`, where `α` is a topological space and `β` is a uniform space, and for any continuous function `f` from `α` to `β`, any type `ι`, any filter `p` on `ι`, any function `F` from `ι` to the space of continuous functions from `α` to `β`, given that `α` is a compact space, the sequence `F` converges to `f` in the compact-open topology (meaning, the `F`-preimages of neighborhoods of `f` are neighborhoods in the filter `p`) if and only if `F` converges uniformly to `f` with respect to the filter `p` (meaning, for any entourage of the diagonal in `β`, eventually for all `n` in the filter `p` and all `x` in `α`, the pair `(f x, F n x)` is in the entourage).
In simpler terms, this theorem establishes an equivalence between two types of convergence - convergence in the compact-open topology and uniform convergence - for sequences of continuous functions on a compact space.
More concisely: For a compact space X, a uniform space Y, and a continuous function f : X → Y, a sequence (F\_n) of continuous functions from X to Y converges to f in the compact-open topology if and only if it converges uniformly to f with respect to any filter on the natural numbers.
|
ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn
theorem ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn :
∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {ι : Type u₃} {p : Filter ι}
{F : ι → C(α, β)} {f : C(α, β)},
Filter.Tendsto F p (nhds f) ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K
The theorem states that for any types `α`, `β`, and `ι`, given a topological space on `α`, a uniform space on `β`, a filter `p` on `ι`, a family of continuous functions `F` from `ι` to the continuous maps from `α` to `β`, and a continuous map `f` from `α` to `β`, the family of functions `F` tends to `f` in the compact-open topology if and only if for all compact sets `K` in `α`, the sequence of functions `F i` tends uniformly on `K` towards the function represented by `f`. In other words, the compact-open topology on the space of continuous functions from `α` to `β` agrees with the topology of uniform convergence on compact sets.
More concisely: The compact-open topology on the space of continuous functions from `α` to `β` coincides with the topology of uniform convergence on compact sets.
|
ContinuousMap.tendsto_iff_tendstoLocallyUniformly
theorem ContinuousMap.tendsto_iff_tendstoLocallyUniformly :
∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {f : C(α, β)} {ι : Type u₃}
{p : Filter ι} {F : ι → C(α, β)} [inst_2 : WeaklyLocallyCompactSpace α],
Filter.Tendsto F p (nhds f) ↔ TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p
This theorem states that, in a weakly locally compact space, the convergence of a sequence of functions `F` to a function `f` in the compact-open topology is equivalent to the condition that `F` converges locally uniformly to `f` with respect to a filter `p`. Here, "locally uniform convergence" means that for every given entourage of the diagonal `u` and for any point `x`, there exists a neighborhood of `x` in which all the functions `F` eventually stay within `u` of `f`. The theorem also indicates that the implication from locally uniform convergence to convergence in the compact-open topology holds in any topological space.
More concisely: In a weakly locally compact space, a sequence of functions converges to a limit in the compact-open topology if and only if it converges locally uniformly to the limit with respect to some filter.
|