Continuous.uniformContinuous_of_tendsto_cocompact
theorem Continuous.uniformContinuous_of_tendsto_cocompact :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {x : β},
Continuous f → Filter.Tendsto f (Filter.cocompact α) (nhds x) → UniformContinuous f
The theorem `Continuous.uniformContinuous_of_tendsto_cocompact` states that for any two types `α` and `β` with uniform spaces, and for any function `f` from `α` to `β` and any point `x` in `β`, if the function `f` is continuous and it converges to `x` with respect to the filter generated by the complements of compact sets in `α` (i.e., `f` tends to `x` when all points in `α` are getting closer to the edges of compact sets), then the function `f` is uniformly continuous. Uniform continuity means that the rate of change of `f` is bounded across its entire domain, or equivalently, that `f` preserves closeness: points that are close together in `α` get mapped to points that are close together in `β`.
More concisely: If a continuous function from a uniform space to another uniform space tends to a point with respect to the filter generated by the complements of compact sets, then it is uniformly continuous.
|
ContinuousOn.tendstoUniformly
theorem ContinuousOn.tendstoUniformly :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β]
[inst_2 : LocallyCompactSpace α] [inst_3 : CompactSpace β] [inst_4 : UniformSpace γ] {f : α → β → γ} {x : α}
{U : Set α}, U ∈ nhds x → ContinuousOn (↿f) (U ×ˢ Set.univ) → TendstoUniformly f (f x) (nhds x)
The theorem `ContinuousOn.tendstoUniformly` states that given a family of functions mapping from two variables `α` and `β` to `γ`, the family tends uniformly towards its value at a particular point `x` if the space `α` is locally compact, the space `β` is compact, and the function `f` is continuous on the product of some neighborhood `U` of `x` and the entire space of `β`. Here, "tends uniformly" means that for any given "closeness" criterion, there is a point in the neighborhood filter of `x` beyond which all the functions in the family satisfy that criterion for all points in the spaces `α` and `β`. The theorem asserts this under the condition that `U` is a neighborhood of `x` and the function is continuous on the product of `U` and the universal set of `β`.
More concisely: Given a continuous family of functions from a locally compact space `α` to a compact space `β`, if the familyUniformly converges to a function `f` on a neighborhood `U` of a point `x` in `α`, then for any ε > 0, there exists a neighborhood `V` of `x` in `U` such that for all `y` in `V` and all `β`-valued functions `g` in the family, the distance between `f(x)` and `g(y)` is less than ε.
|
IsCompact.uniformContinuousOn_of_continuous
theorem IsCompact.uniformContinuousOn_of_continuous :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {s : Set α} {f : α → β},
IsCompact s → ContinuousOn f s → UniformContinuousOn f s
The Heine-Cantor theorem states that a function that is continuous on a compact set within a uniform space is uniformly continuous. In more detail, given a set `s` from the type `α`, which is equipped with a uniform space structure, and a function `f` from `α` to `β` (where `β` is also a uniform space), if the set `s` is compact and the function `f` is continuous on `s`, then the function `f` is uniformly continuous on `s`. This means that, if any two points in `s` are sufficiently close, their images under `f` are also close, regardless of their specific location in `s`.
More concisely: A continuous function on a compact uniform space is uniformly continuous.
|
Continuous.tendstoUniformly
theorem Continuous.tendstoUniformly :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β]
[inst_2 : WeaklyLocallyCompactSpace α] [inst_3 : CompactSpace β] [inst_4 : UniformSpace γ] (f : α → β → γ),
Continuous ↿f → ∀ (x : α), TendstoUniformly f (f x) (nhds x)
The theorem states that for any continuous family of functions from `α` to `β → γ`, where `α` is a weakly locally compact space and `β` is a compact space, the function family tends uniformly towards its value at a given point `x` in `α`. In more detail, the functions get closer and closer to their value at `x` (in the sense of the topology defined by the uniform space structure), as you look at neighborhoods of `x` that shrink towards `x`. This property is called uniform convergence and is typically found in contexts where we consider a series of approximations to a function.
More concisely: For any continuous family of functions from a weakly locally compact space to a compact space, the functions uniformly converge to their value at a point as neighborhoods of that point shrink to the point.
|
HasCompactSupport.is_zero_at_infty
theorem HasCompactSupport.is_zero_at_infty :
∀ {α : Type u_1} {γ : Type u_3} [inst : UniformSpace α] {f : α → γ} [inst_1 : TopologicalSpace γ] [inst_2 : Zero γ],
HasCompactSupport f → Filter.Tendsto f (Filter.cocompact α) (nhds 0)
The theorem `HasCompactSupport.is_zero_at_infty` states that for any function `f` from a uniform space `α` to a topological space `γ` with a zero element, if `f` has compact support, then `f` tends to zero at infinity. In other words, for every neighborhood of zero in `γ`, the preimage under `f` of this neighborhood is eventually outside a compact set in `α`. This essentially means that `f` gets arbitrarily close to zero when moving away from a compact set in `α`.
More concisely: For any uniform space homomorphism from a uniform space with a zero element to a topological space with a zero element having compact support, the preimage of every neighborhood of zero in the target space is eventually disjoint from any compact set in the domain, i.e., the function tends to zero at infinity.
|
nhdsSet_diagonal_eq_uniformity
theorem nhdsSet_diagonal_eq_uniformity :
∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : CompactSpace α], nhdsSet (Set.diagonal α) = uniformity α := by
sorry
The theorem `nhdsSet_diagonal_eq_uniformity` states that in a compact uniform space, the uniform structure is completely determined by the topology. More specifically, the uniformity or the set of all entourages (a collection of all possible "distances" in the space) is equivalent to the filter of neighborhoods of the diagonal of the space. The diagonal of a space is the set of all pairs where both elements are the same. This result encapsulates the interplay between the uniform and topological structures in a compact space.
More concisely: In a compact uniform space, the uniformity is equivalent to the filter of neighborhoods of the diagonal.
|
HasCompactMulSupport.is_one_at_infty
theorem HasCompactMulSupport.is_one_at_infty :
∀ {α : Type u_1} {γ : Type u_3} [inst : UniformSpace α] {f : α → γ} [inst_1 : TopologicalSpace γ] [inst_2 : One γ],
HasCompactMulSupport f → Filter.Tendsto f (Filter.cocompact α) (nhds 1)
The theorem `HasCompactMulSupport.is_one_at_infty` states that if a function `f` has compact multiplicative support, then `f` tends to 1 at infinity. In other words, for a function `f` from a uniform space `α` to a topological space `γ` equipped with a multiplication operation, if the closure of the set where `f` is not equal to `1` is compact, then for every neighborhood of `1` in `γ`, there exists a complement of a compact set in `α` such that the image of this set under `f` is contained within this neighborhood. This is a rigorous formalization of the intuitive idea that `f` gets arbitrarily close to `1` outside of some compact set in `α`.
More concisely: If a function from a uniform space to a topological space with multiplication has compact multiplicative support, then for every neighborhood of 1 in the target space, there exists a complement of a compact set in the domain such that the image of that set is contained in the neighborhood.
|
compactSpace_uniformity
theorem compactSpace_uniformity :
∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : CompactSpace α], uniformity α = ⨆ x, nhds (x, x)
This theorem states that for any compact uniform space, the topology is what determines the uniform structure. In other words, the uniformity (a filter on the product of the space with itself) is exactly the sup (join of all) neighborhoods of each point in the diagonal. This means that the uniform structure is completely determined by how close points are to each other in the topology, and the concept of "closeness" is captured by the neighborhoods of the diagonal in the space.
More concisely: For any compact uniform space, the uniformity is the supremum of the neighborhood filters of the diagonal in the product topology.
|
CompactSpace.uniformContinuous_of_continuous
theorem CompactSpace.uniformContinuous_of_continuous :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : CompactSpace α]
{f : α → β}, Continuous f → UniformContinuous f
The Heine-Cantor theorem states that if you have a function `f` mapping from a compact uniform space `α` to any other uniform space `β`, and this function is continuous, then it is also uniformly continuous. In mathematical terms, a function is uniformly continuous on a set if, given any positive distance, there is a distance such that any two points in the set less than this distance apart are mapped to points less than the positive distance apart. In this context, a compact space is a topological space in which every open cover has a finite subcover.
More concisely: If `f` is a continuous function from the compact uniform space `α` to the uniform space `β`, then `f` is uniformly continuous.
|
CompactSpace.uniformEquicontinuous_of_equicontinuous
theorem CompactSpace.uniformEquicontinuous_of_equicontinuous :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {ι : Type u_4} {F : ι → β → α}
[inst_2 : CompactSpace β], Equicontinuous F → UniformEquicontinuous F
This theorem states that if we have a family of functions `F` indexed by `ι` that maps from a compact uniform space `β` to another uniform space `α`, and this family of functions is equicontinuous (meaning it is equicontinuous at every point in `β`), then this family of functions `F` is also uniformly equicontinuous. In other words, for any entourage in the uniform space `α`, there is an entourage in `β` such that, whenever two points are close in `β`, the images of these points under any function from the family `F` are close in `α`.
More concisely: If `F:` `β` → `α^ι` is a family of functions from a compact uniform space `β` to a uniform space `α` that is equicontinuous, then `F` is uniformly equicontinuous.
|
IsCompact.mem_uniformity_of_prod
theorem IsCompact.mem_uniformity_of_prod :
∀ {α : Type u_4} {β : Type u_5} {E : Type u_6} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : UniformSpace E] {f : α → β → E} {s : Set α} {k : Set β} {q : α} {u : Set (E × E)},
IsCompact k →
ContinuousOn (Function.uncurry f) (s ×ˢ k) →
q ∈ s → u ∈ uniformity E → ∃ v ∈ nhdsWithin q s, ∀ p ∈ v, ∀ x ∈ k, (f p x, f q x) ∈ u
The theorem `IsCompact.mem_uniformity_of_prod` states that if we have a product space `α × β` and a function `f` that is continuous on the product of set `s` and a compact set `k`, then for any element `q` in `s`, the function `f` is transversely uniformly continuous. In other words, if there exists an element `p` in `s` that is sufficiently close to `q`, then for all elements `x` in the compact set `k`, the image of `(p, x)` under `f` is uniformly close to the image of `(q, x)` under `f` in `E`. This uniform closeness in `E` is given by a certain set `u` from the uniformity structure of `E`.
More concisely: If a continuous function on the product of a set and a compact set is restricted to the set, then it is uniformly continuous on that set. (In the context of the theorem, the uniform continuity holds for elements in the compact set and for elements in the set that are sufficiently close to each other.)
|
IsCompact.uniformContinuousAt_of_continuousAt
theorem IsCompact.uniformContinuousAt_of_continuousAt :
∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {r : Set (β × β)} {s : Set α},
IsCompact s →
∀ (f : α → β),
(∀ a ∈ s, ContinuousAt f a) → r ∈ uniformity β → {x | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ uniformity α
The theorem states that if we have a set `s` which is compact and a function `f` that is continuous at all points in the set `s`, then the function `f` is uniformly continuous at the set `s`. In other words, for any `x` in `s` and any `y` close to `x`, `f(x)` is close to `f(y)`. This is a stronger claim than saying `f` is uniformly continuous on `s`, because it holds even if `y` is not in `s`. The closeness of `f(x)` and `f(y)` is defined in terms of a given relationship `r`, which is from the uniformity of the codomain space, and the closeness of `x` and `y` is defined in terms of the uniformity of the domain space.
More concisely: If a compact set `s` and a continuous function `f` over `s` satisfy the uniformity condition that for every open set containing `f(x)` in the codomain and every open set containing `x` in the domain, there exists an open set in the domain containing both `x` and `y` such that `|f(x) - f(y)| < r`, then `f` is uniformly continuous on the set `s` and even outside it.
|