cauchy_nhds
theorem cauchy_nhds : ∀ {α : Type u} [uniformSpace : UniformSpace α] {a : α}, Cauchy (nhds a)
This theorem states that for any type `α` that has a `UniformSpace` structure, and for any element `a` of type `α`, the neighborhood filter at `a` is a Cauchy filter. In terms of mathematics, it means that in any uniform space, every neighborhood of a point forms a Cauchy filter, which generalizes the concept of a Cauchy sequence to arbitrary uniform spaces.
More concisely: In any uniform space, the neighborhood filter of any point is a Cauchy filter.
|
IsClosed.isComplete
theorem IsClosed.isComplete :
∀ {α : Type u} [uniformSpace : UniformSpace α] [inst : CompleteSpace α] {s : Set α}, IsClosed s → IsComplete s := by
sorry
This theorem states that for any type `α` equipped with a uniform space and a complete space structure, any closed set `s` is a complete set. In the context of analysis, a set is considered "complete" if every Cauchy filter that takes values in the set has a limit within the set. The theorem tells us that if we have a closed set in a complete space, then it also has this property. This means, intuitively, that sequences in the set which should have a limit do indeed have a limit, and that limit is also within the set.
More concisely: In a complete uniform space, every closed set is a complete set, meaning that every Cauchy filter with values in the set has a limit within the set.
|
UniformSpace.complete_of_convergent_controlled_sequences
theorem UniformSpace.complete_of_convergent_controlled_sequences :
∀ {α : Type u} [uniformSpace : UniformSpace α] [inst : (uniformity α).IsCountablyGenerated] (U : ℕ → Set (α × α)),
(∀ (n : ℕ), U n ∈ uniformity α) →
(∀ (u : ℕ → α),
(∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Filter.Tendsto u Filter.atTop (nhds a)) →
CompleteSpace α
This theorem states that a uniform space is complete if it satisfies two conditions:
(a) its uniformity filter has a countable basis. This is represented in Lean 4 by the typeclass instance `Filter.IsCountablyGenerated (uniformity α)`.
(b) any sequence in the space that satisfies a "controlled" version of the Cauchy condition converges. Specifically, for any sequence `u : ℕ → α`, if for every natural number `N` and every pair of indices `m` and `n` greater than or equal to `N`, `(u m, u n)` falls within the `N`th set `U N` from the countable basis of the uniformity filter, then there exists an element `a` in the space such that the sequence `u` converges to `a` at infinity. This is represented by `∃ a, Filter.Tendsto u Filter.atTop (nhds a)` in Lean 4.
If these conditions are met, then the space is a complete space, as indicated by `CompleteSpace α` in Lean 4.
More concisely: A uniform space is complete if and only if its uniformity filter has a countable basis and every Cauchy sequence in the space converges to a limit in the space.
|
isCompact_iff_totallyBounded_isComplete
theorem isCompact_iff_totallyBounded_isComplete :
∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α}, IsCompact s ↔ TotallyBounded s ∧ IsComplete s := by
sorry
This theorem states that for any set `s` in a uniform space `α`, the set is compact if and only if it is both totally bounded and complete. In other words, a set is compact when, given any nontrivial filter that contains the set, there exists an element within the set such that every set of the filter meets every neighborhood of this element, and this is equivalent to the set being totally bounded, where for every entourage there exists a finite set of points such that every element of the original set is near to some element of the finite set, and complete, where any Cauchy filter that includes the set has a limit in the set.
More concisely: A set in a uniform space is compact if and only if it is both totally bounded and complete.
|
Cauchy.map
theorem Cauchy.map :
∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] {f : Filter α} {m : α → β},
Cauchy f → UniformContinuous m → Cauchy (Filter.map m f)
The theorem `Cauchy.map` states that for any two types `α` and `β` equipped with a uniform space structure, a filter `f` on `α`, and a function `m : α → β`, if the filter `f` is Cauchy and the function `m` is uniformly continuous, then the filter obtained by mapping `f` through `m` is also Cauchy. In other words, mapping a Cauchy filter through a uniformly continuous function preserves the property of being Cauchy.
More concisely: If `f` is a Cauchy filter on type `α` with uniform structure, and `m : α → β` is a uniformly continuous function, then the filter `m``⁻¹````(f)` obtained by mapping `f` through `m` is also Cauchy.
|
Filter.Tendsto.cauchySeq
theorem Filter.Tendsto.cauchySeq :
∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : SemilatticeSup β] [inst_1 : Nonempty β]
{f : β → α} {x : α}, Filter.Tendsto f Filter.atTop (nhds x) → CauchySeq f
The theorem `Filter.Tendsto.cauchySeq` states that for any types `α` and `β`, given a uniform space on `α`, a semilattice structure on `β`, and assuming that `β` is nonempty, if we have a function `f` from `β` to `α` and an element `x` of `α`, then if `f` tends to `x` at the limit `∞` (meaning that the image of `f` approaches `x` when the argument of `f` goes to infinity), it implies that `f` is a Cauchy sequence. In other words, when the values of `f` get arbitrarily close to `x` as we take larger and larger values from `β`, then `f` is considered a Cauchy sequence, i.e., the elements of the sequence become arbitrarily close to each other as we progress further into the sequence.
More concisely: If a function from a semilattice to a uniform space tends to a limit as its argument approaches infinity, then it is a Cauchy sequence.
|
TotallyBounded.closure
theorem TotallyBounded.closure :
∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α}, TotallyBounded s → TotallyBounded (closure s) := by
sorry
The theorem states that the closure of a totally bounded set is totally bounded. In more detail, for any type `α` equipped with a uniform space structure and any set `s` of elements of type `α`, if `s` is totally bounded (i.e., for any given entourage, there exists a finite set of points such that each element of `s` is near to an element of this finite set according to the entourage), then the closure of `s` (the smallest closed set containing `s`) is also totally bounded. This means that the property of being totally bounded is preserved under the operation of taking closures.
More concisely: The closure of a totally bounded set in a uniform space is still totally bounded.
|
cauchySeq_tendsto_of_isComplete
theorem cauchySeq_tendsto_of_isComplete :
∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : Preorder β] {K : Set α},
IsComplete K →
∀ {u : β → α}, (∀ (n : β), u n ∈ K) → CauchySeq u → ∃ v ∈ K, Filter.Tendsto u Filter.atTop (nhds v)
The theorem `cauchySeq_tendsto_of_isComplete` states that if `K` is a complete subset of a uniform space `α` (i.e., every Cauchy filter in `K` has a limit within `K`), then any Cauchy sequence `u` in `K` (a sequence where elements get arbitrarily close as the sequence progresses) will converge to some point `v` in `K`. In other words, for any Cauchy sequence `u` in `K`, we can find an element `v` in `K` such that `u` tends to `v` at infinity, where "tends to" is defined in the sense of filters (i.e., for every neighborhood of `v`, there exists some point in the sequence beyond which all elements are in that neighborhood).
More concisely: If `K` is a complete subset of a uniform space, then every Cauchy sequence in `K` converges to some limit in `K`.
|
Cauchy.prod
theorem Cauchy.prod :
∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] {f : Filter α} {g : Filter β},
Cauchy f → Cauchy g → Cauchy (f ×ˢ g)
The theorem `Cauchy.prod` states that for any two types `α` and `β` with uniform spaces, if `f` is a Cauchy filter on `α` and `g` is a Cauchy filter on `β`, then the product filter `(f ×ˢ g)` on the product space `α × β` is also a Cauchy filter. In mathematical terms, this theorem ensures that the property of being Cauchy is preserved under taking products in the context of uniform spaces.
More concisely: Given Cauchy filters `f` on type `α` and `g` on type `β` in a uniform space, their product `f ×ˢ g` is also a Cauchy filter.
|
le_nhds_of_cauchy_adhp_aux
theorem le_nhds_of_cauchy_adhp_aux :
∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} {x : α},
(∀ s ∈ uniformity α, ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ y, (x, y) ∈ s ∧ y ∈ t) → f ≤ nhds x
This theorem, named `le_nhds_of_cauchy_adhp_aux`, is in the context of a type `α` which has a uniform space structure. The theorem states that given any filter `f` on `α` and any point `x` in `α`, if for every entourage `s` (which is a set in the uniformity of `α`), there exists a set `t` in `f` such that two conditions hold: (1) the product of `t` with itself is a subset of `s` (implying that `t` has a diameter no larger than `s`), and (2) there exists a point `y` such that `(x, y)` is in `s` and `y` is in `t`, then the filter `f` converges to `x`. In simpler words, if every neighborhood of `x` contains a set from the filter that is "small" enough and contains a point close to `x`, then the filter converges to `x`.
More concisely: If for every entourage containing `(x, y)` in `α` and every filter `f` on `α`, there exists a set in `f` whose diameter is less than or equal to the entourage and contains a point `y'` with `(x, y')` in the entourage, then `f` converges to `x`.
|
UniformContinuous.comp_cauchySeq
theorem UniformContinuous.comp_cauchySeq :
∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} [inst : UniformSpace β]
[inst_1 : Preorder γ] {f : α → β}, UniformContinuous f → ∀ {u : γ → α}, CauchySeq u → CauchySeq (f ∘ u)
This theorem states that if a function `f` from type `α` to type `β` is uniformly continuous, and if a sequence `u` from type `γ` to type `α` is a Cauchy sequence, then the composition of `f` and `u` (i.e., `f ∘ u`) is also a Cauchy sequence. In other words, applying a uniformly continuous function to a Cauchy sequence results in a Cauchy sequence. This holds for any types `α`, `β`, and `γ` where `α` and `β` are equipped with a uniform space structure and `γ` is equipped with a pre-order structure.
More concisely: If `f` is a uniformly continuous function from `α` to `β` and `u` is a Cauchy sequence in `α`, then the composition `f ∘ u` is a Cauchy sequence in `β`.
|
Cauchy.mono
theorem Cauchy.mono :
∀ {α : Type u} [uniformSpace : UniformSpace α] {f g : Filter α} [hg : g.NeBot], Cauchy f → g ≤ f → Cauchy g := by
sorry
The theorem `Cauchy.mono` states that for any uniform space `α` and any two filters `f` and `g` on `α` (where `g` is guaranteed not to be the bottom filter), if `f` is a Cauchy filter and `g` is a subset of `f`, then `g` is also a Cauchy filter. To put it simply, this theorem shows that the Cauchy property of a filter is preserved under taking subsets. The preservation of the Cauchy property is important because it ensures that when we restrict our attention to a smaller filter, we can still make the same conclusions about the closeness of the elements of the filter.
More concisely: If `α` is a uniform space, `f` is a Cauchy filter on `α`, and `g` is a subset of `f` not equal to the bottom filter, then `g` is also a Cauchy filter.
|
Filter.HasBasis.totallyBounded_iff
theorem Filter.HasBasis.totallyBounded_iff :
∀ {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {U : ι → Set (α × α)},
(uniformity α).HasBasis p U →
∀ {s : Set α}, TotallyBounded s ↔ ∀ (i : ι), p i → ∃ t, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}
This theorem states that for a given type `α` with an associated uniform space and a given filter basis on `α × α` determined by a property `p` and a set function `U`, a set `s` of type `α` is totally bounded if and only if for every `i` where `p(i)` is true, there exists a finite set `t` such that every element in `s` is close, with closeness defined by `U(i)`, to at least one element in `t`. In other words, no matter which condition `i` from the filter basis we use to define closeness, we can always find a finite set of reference points such that all points in our set are close to at least one reference point.
More concisely: A set `s` in a uniform space `α` is totally bounded with respect to a filter basis determined by property `p` and set function `U` if and only if for each `i` where `p(i)` holds, there exists a finite set `t` such that every element in `s` is close to some element in `t` using the closeness relation defined by `U(i)`.
|
cauchySeq_iff_tendsto
theorem cauchySeq_iff_tendsto :
∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : Nonempty β] [inst : SemilatticeSup β]
{u : β → α}, CauchySeq u ↔ Filter.Tendsto (Prod.map u u) Filter.atTop (uniformity α)
The theorem `cauchySeq_iff_tendsto` states that for any types `α` and `β`, with `α` being a uniform space and `β` being a nonempty semilattice sup, and any function `u` from `β` to `α`, the sequence `u` is a Cauchy sequence if and only if the map of pairs `(u, u)` tends to the uniformity of `α` as `β` tends to infinity. This theorem ties the notion of a sequence being Cauchy (i.e., the terms of the sequence becoming arbitrarily close to each other as the sequence progresses) with the notion of a function tending to a limit (in this case, the uniformity of the space `α`).
More concisely: A sequence in a uniform space is Cauchy if and only if the function mapping each term to itself tends to the uniformity of the space as the sequence index approaches infinity.
|
totallyBounded_iff_subset
theorem totallyBounded_iff_subset :
∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α},
TotallyBounded s ↔ ∀ d ∈ uniformity α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
This theorem states that for any set `s` of a certain type `α`, where `α` is equipped with a uniform space structure, the set `s` is totally bounded if and only if for every entourage `d` in the uniformity of `α`, there exists a finite subset `t` of `s` such that every element of `s` is `d`-near to some element of `t`. More explicitly, for each `d` in the uniformity of `α`, there exists a finite set `t` such that `t` is a subset of `s`, and for every element in `s`, there exists an element in `t` such that the pair of this element and the element in `t` belongs to `d`.
More concisely: A uniform space `(α, δ)` is totally bounded if and only if for every entourage `d` in `δ`, there exists a finite subset `t` of `α` such that every element in `α` is `d`-near to some element in `t`.
|
TotallyBounded.image
theorem TotallyBounded.image :
∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] {f : α → β} {s : Set α},
TotallyBounded s → UniformContinuous f → TotallyBounded (f '' s)
This theorem states that if you have a totally bounded set in a uniform space (a type of topological space), and a uniformly continuous function from that space to another uniform space, then the image of that totally bounded set under the uniformly continuous function will also be totally bounded. In other words, the property of being totally bounded is preserved under a uniformly continuous transformation. This can be represented mathematically as: for all set `s` in type `α` and function `f: α → β`, if `s` is totally bounded and `f` is uniformly continuous, then the image of `s` under `f` (denoted `f '' s`) is totally bounded.
More concisely: If `s` is a totally bounded subset of a uniform space and `f:` `α` `→` `β` is a uniformly continuous function, then `f''s` is a totally bounded subset of `β`.
|
SequentiallyComplete.setSeq_mem
theorem SequentiallyComplete.setSeq_mem :
∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)}
(U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ), SequentiallyComplete.setSeq hf U_mem n ∈ f
This theorem states that for any type `α` that has a uniform space structure, any Cauchy filter `f` on `α`, and any sequence `U` of sets of ordered pairs from `α` such that each `U n` is in the uniformity of `α`, the set sequence created by `SequentiallyComplete.setSeq` applied to the filter `f`, the sequence `U`, and any natural number `n` is a member of the filter `f`. In other words, it guarantees that the sets we construct through the `SequentiallyComplete.setSeq` function from a Cauchy filter and a sequence of entourages always belong to the original filter.
More concisely: For any Cauchy filter on a uniform space and any sequence of entourages in its uniformity, the sequence of sets generated by applying `SequentiallyComplete.setSeq` belongs to the Cauchy filter.
|
Cauchy.comap'
theorem Cauchy.comap' :
∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] {f : Filter β} {m : α → β},
Cauchy f →
Filter.comap (fun p => (m p.1, m p.2)) (uniformity β) ≤ uniformity α →
(Filter.comap m f).NeBot → Cauchy (Filter.comap m f)
The theorem `Cauchy.comap'` states that for any two types `α` and `β` equipped with uniform space structures, a filter `f` on `β`, and a function `m` from `α` to `β`, if `f` is a Cauchy filter, the filter obtained by comapping the function that takes a pair `p` and returns a pair with the images of the components of `p` under `m` through the uniformity of `β` is less than or equal to the uniformity of `α`, and the filter obtained by comapping `m` through `f` is not bottom, then this last filter is a Cauchy filter.
In other words, this theorem provides a condition under which the image of a Cauchy filter under a mapping is still a Cauchy filter. This is important in studying the continuity and convergence properties of functions between uniform spaces.
More concisely: Given uniform spaces (α, δα) and (β, δβ), a Cauchy filter f on β, and a continuous function m : α → β, if f is a Cauchy filter and the image filter of f under m through δβ is not bottom and is less than or equal to δα, then the image filter of m under f through δα is also a Cauchy filter.
|
Filter.HasBasis.cauchySeq_iff'
theorem Filter.HasBasis.cauchySeq_iff' :
∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Sort u_1} [inst : Nonempty β]
[inst : SemilatticeSup β] {u : β → α} {p : γ → Prop} {s : γ → Set (α × α)},
(uniformity α).HasBasis p s → (CauchySeq u ↔ ∀ (i : γ), p i → ∃ N, ∀ n ≥ N, (u n, u N) ∈ s i)
The theorem `Filter.HasBasis.cauchySeq_iff'` states that for any types `α` and `β`, where `α` is equipped with a uniform space structure, and `β` is a nonempty, semilattice sup (a partially ordered set with a least upper bound for any two elements), and for any function `u` from `β` to `α`, and for any properties `p` indexed by some type `γ` and any sets `s` of `α` pairs indexed by `γ`, if the uniformity of `α` has a filter basis consisting of the sets `s i` for which `p i` holds, then the function `u` is a Cauchy sequence if and only if for every `i` in `γ` such that `p i` holds, there exists some `N` in `β` such that for all `n` in `β` greater than or equal to `N`, the pair `(u n, u N)` belongs to the set `s i`. In simpler terms, this theorem provides a condition for a sequence to be Cauchy in terms of a basis for the uniformity.
More concisely: A sequence in a uniform space with respect to a filter basis consisting of sets indexed by a semilattice sup-type, where each set contains pairs of sequence elements satisfying a given property, is a Cauchy sequence if and only if for each index in the property domain, there exists a supremum element such that the sequence converges to that element within the set.
|
cauchySeq_tendsto_of_complete
theorem cauchySeq_tendsto_of_complete :
∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : Preorder β] [inst_1 : CompleteSpace α]
{u : β → α}, CauchySeq u → ∃ x, Filter.Tendsto u Filter.atTop (nhds x)
This theorem states that for any Cauchy sequence `u` in a complete space `α` (with a uniform structure and a preorder on the indexing set `β`), there exists some element `x` in `α` such that `u` converges to `x` as `β` goes to infinity. In mathematical terms, if a sequence is Cauchy (i.e., the elements get arbitrarily close to each other as we go further in the sequence) and the space is complete (i.e., every Cauchy sequence converges), then the sequence must converge to some point in the space. The convergence is expressed using the `Filter.Tendsto` predicate, which says that for every neighborhood of `x`, there exists a point in the sequence beyond which all the elements are in that neighborhood.
More concisely: Every Cauchy sequence in a complete space converges to a limit in that space.
|
UniformSpace.complete_of_cauchySeq_tendsto
theorem UniformSpace.complete_of_cauchySeq_tendsto :
∀ {α : Type u} [uniformSpace : UniformSpace α] [inst : (uniformity α).IsCountablyGenerated],
(∀ (u : ℕ → α), CauchySeq u → ∃ a, Filter.Tendsto u Filter.atTop (nhds a)) → CompleteSpace α
This theorem states that for any type `α` that has a `UniformSpace` structure and a countably generated uniformity filter, if all Cauchy sequences in `α` have a limit in `α` (i.e., for each Cauchy sequence `u`, there exists an element `a` in `α` such that `u` tends to `a` as `n` goes to infinity), then `α` is a complete space. In mathematical terms, this theorem asserts that a sequentially complete uniform space with a countable basis of the uniformity filter is complete. This is a fundamental result in the theory of metric and uniform spaces, asserting that sequential completeness (every Cauchy sequence converges) and completeness (every Cauchy filter converges) are equivalent conditions in such spaces.
More concisely: A sequentially complete uniform space with a countable basis for its uniformity filter is a complete space.
|
CompleteSpace.complete
theorem CompleteSpace.complete :
∀ {α : Type u} [inst : UniformSpace α] [self : CompleteSpace α] {f : Filter α}, Cauchy f → ∃ x, f ≤ nhds x := by
sorry
In the context of a complete uniform space, the theorem states that every Cauchy filter converges to a point. More specifically, given a type `α` equipped with a uniform space structure and the property of being a complete space, for any filter `f` over `α` that satisfies the Cauchy condition (i.e., for each entourage, there exists a subset `s` in the filter such that the product `s × s` is a subset of the entourage), there exists an element `x` of `α` such that the filter `f` is a subset of the neighborhood filter at `x`. This indicates that the points in the Cauchy filter `f` get arbitrarily close to `x`, or in other words, the Cauchy filter `f` converges to `x`.
More concisely: In a complete uniform space, every Cauchy filter converges to a point.
|
cauchy_map_iff_exists_tendsto
theorem cauchy_map_iff_exists_tendsto :
∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : CompleteSpace α] {l : Filter β} {f : β → α}
[inst : l.NeBot], Cauchy (Filter.map f l) ↔ ∃ x, Filter.Tendsto f l (nhds x)
The theorem `cauchy_map_iff_exists_tendsto` states that for any types `α` and `β` where `α` is a uniform and complete space, given a filter `l` over `β` that is not the bottom filter, and a function `f` mapping from `β` to `α`, the filter formed by mapping `f` over `l` is Cauchy if and only if there exists an element `x` for which `f` tends to (in the sense of filters) the neighborhood filter at `x`. In mathematical terms, this theorem connects the property of a filter being Cauchy with the existence of a limit in the topological sense, under the action of a function.
More concisely: A filter `l` over a uniform and complete space `β` maps to a Cauchy filter in `α` under a function `f:` `β` → `α` if and only if there exists an `x` in `α` such that `f` tends to the neighborhood filter at `x`.
|
completeSpace_iff_isComplete_univ
theorem completeSpace_iff_isComplete_univ :
∀ {α : Type u} [uniformSpace : UniformSpace α], CompleteSpace α ↔ IsComplete Set.univ
The theorem `completeSpace_iff_isComplete_univ` states that for any type `α` that is equipped with a uniform space structure, `α` is a complete space if and only if the universal set of `α` is complete. In the context of this theorem, a set is complete if any Cauchy filter on the set has a limit within the set, and a space is complete if every Cauchy filter converges to a point within the space. The universal set of `α` is the set containing all elements of `α`. In essence, this theorem links the property of completeness of the whole space with the completeness of the universal set in that space.
More concisely: A uniform space `α` is complete if and only if its universal set is complete.
|
UniformSpace.secondCountable_of_separable
theorem UniformSpace.secondCountable_of_separable :
∀ (α : Type u) [uniformSpace : UniformSpace α] [inst : (uniformity α).IsCountablyGenerated]
[inst : TopologicalSpace.SeparableSpace α], SecondCountableTopology α
This theorem states that a separable uniform space, whose uniformity filter is countably generated, is second countable. In other words, we can obtain a countable basis for such a space by considering the balls centered at points in a dense subset, with "radii" from a countable, open, symmetric, antitone basis of the uniformity on the space. Note that this is not registered as an instance, because there is already an instance that transforms second countable spaces to separable spaces, and we want to avoid loops.
More concisely: A separable uniform space with a countably generated uniformity filter is second countable.
|
cauchy_iff
theorem cauchy_iff :
∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α},
Cauchy f ↔ f.NeBot ∧ ∀ s ∈ uniformity α, ∃ t ∈ f, t ×ˢ t ⊆ s
The theorem named `cauchy_iff` states that for any type `α` that has a uniform space structure, and for any filter `f` on `α`, the filter `f` is Cauchy (in the sense defined above) if and only if two conditions are met. The first condition is that `f` is not the bottom filter, denoted by `Filter.NeBot f`. The second condition is that for every set `s` in the uniformity of `α`, there exists a set `t` in `f` such that the product of `t` with itself is a subset of `s`. This theorem essentially provides a characterisation of Cauchy filters in terms of non-bottom filters and the uniformity of the underlying space.
More concisely: For any uniform space `(α, Υ)`, a filter `f` on `α` is Cauchy if and only if it is not the bottom filter and for every `s ∈ Υ`, there exists `t ∈ f` such that `t × t ⊆ s`.
|
completeSpace_of_isComplete_univ
theorem completeSpace_of_isComplete_univ :
∀ {α : Type u} [uniformSpace : UniformSpace α], IsComplete Set.univ → CompleteSpace α
The theorem `completeSpace_of_isComplete_univ` states that if the universal set (`univ`) is complete in a given uniform space, then the space itself is a complete space. In the context of this theorem, a set is considered "complete" if any Cauchy filter on that set has a limit within the set. The universal set (`univ`) is the set containing all elements of the space. So if every Cauchy filter on `univ` has a limit within `univ`, then the entire space is a complete space.
More concisely: If the universal set of a uniform space is complete, then the space is complete.
|
Filter.HasBasis.cauchy_iff
theorem Filter.HasBasis.cauchy_iff :
∀ {α : Type u} [uniformSpace : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {s : ι → Set (α × α)},
(uniformity α).HasBasis p s →
∀ {f : Filter α}, Cauchy f ↔ f.NeBot ∧ ∀ (i : ι), p i → ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s i
This theorem states that for any type `α` equipped with a uniform space structure, and given a basis of the uniformity filter of `α` indexed by some type `ι` with a predicate `p` and a function `s` mapping to sets of `α × α`, a filter `f` on `α` is Cauchy if and only if it is not the bottom filter and for any index `i` satisfying the predicate `p`, there exists a set `t` in the filter such that for any two elements `x` and `y` in `t`, the pair `(x, y)` is in the set `s i`. This is a generalization of the notion of Cauchy sequences in terms of filters and uniform spaces.
More concisely: A filter on a uniform space is Cauchy if and only if it is not the bottom filter and for each basis element, there exists a set in the filter containing two elements with that basis element as their uniform distance.
|
totallyBounded_subset
theorem totallyBounded_subset :
∀ {α : Type u} [uniformSpace : UniformSpace α] {s₁ s₂ : Set α}, s₁ ⊆ s₂ → TotallyBounded s₂ → TotallyBounded s₁
The theorem `totallyBounded_subset` states that, for any type `α` equipped with a uniform space structure, and given two sets `s₁` and `s₂` of type `α`, if `s₁` is a subset of `s₂` and `s₂` is totally bounded, then `s₁` is also totally bounded. In other words, the property of being totally bounded is preserved under taking subsets. A set is called totally bounded if, for every entourage (a certain kind of subset of the product `α × α`), there exists a finite set of points such that every element of the original set is close (in the sense defined by the entourage) to at least one point in this finite set.
More concisely: If `α` is a uniform space, `s₁` is a subset of totally bounded set `s₂` in `α`, then `s₁` is also totally bounded.
|
tendsto_nhds_of_cauchySeq_of_subseq
theorem tendsto_nhds_of_cauchySeq_of_subseq :
∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : Preorder β] {u : β → α},
CauchySeq u →
∀ {ι : Type u_1} {f : ι → β} {p : Filter ι} [inst_1 : p.NeBot],
Filter.Tendsto f p Filter.atTop →
∀ {a : α}, Filter.Tendsto (u ∘ f) p (nhds a) → Filter.Tendsto u Filter.atTop (nhds a)
The theorem `tendsto_nhds_of_cauchySeq_of_subseq` states that for any Cauchy sequence `u` in a uniform space `α` (with `α` ordered in a certain way), if there exists a subsequence `f` (indexed over some set `ι`) that converges to some limit `a`, then the original sequence `u` also converges to the same limit `a`. Here, the convergence of the subsequence `f` is defined as the fact that for every neighborhood of `a`, there exists a point in the filter `p` (which is assumed to be non-empty) such that all subsequent elements of the sequence are in that neighborhood. Similarly, the convergence of the original sequence is defined as the fact that for every neighborhood of `a`, there exists a point beyond which all elements of the sequence are in that neighborhood.
More concisely: If a Cauchy sequence in a uniform space converges through a subsequence to a limit, then the original sequence converges to the same limit.
|
CauchySeq.totallyBounded_range
theorem CauchySeq.totallyBounded_range :
∀ {α : Type u} [uniformSpace : UniformSpace α] {s : ℕ → α}, CauchySeq s → TotallyBounded (Set.range s)
The theorem states that for any Cauchy sequence 's' of natural numbers in a uniform space 'α', the range of the sequence is totally bounded. In other words, for every sequence 's' where the distance between elements gets arbitrarily small as the sequence progresses, the set of all possible values of the sequence (its range) has the property that for any given distance, there is a finite set of points such that every point in the range is within that distance of some point in this finite set. This theorem is relevant in the fields of analysis and topology, where it contributes to our understanding of limits and convergence.
More concisely: Given a Cauchy sequence of natural numbers in a uniform space, its range is totally bounded, meaning for any distance, there exists a finite set of points such that every point in the range is within that distance of some point in the set.
|
SequentiallyComplete.le_nhds_of_seq_tendsto_nhds
theorem SequentiallyComplete.le_nhds_of_seq_tendsto_nhds :
∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → Set (α × α)}
(U_mem : ∀ (n : ℕ), U n ∈ uniformity α),
(∀ s ∈ uniformity α, ∃ n, U n ⊆ s) →
∀ ⦃a : α⦄, Filter.Tendsto (SequentiallyComplete.seq hf U_mem) Filter.atTop (nhds a) → f ≤ nhds a
This theorem states that for any type `α` with a uniform space structure and a filter `f` which is Cauchy, along with a sequence of sets `U` with each `U n` being part of the uniformity of `α`, if for every set `s` in the uniformity of `α` there exists an `n` such that `U n` is a subset of `s`, and if `a` is a point in `α` such that the sequence `SequentiallyComplete.seq` converges to `a` as `n` approaches infinity, then `f` is less than or equal to the neighborhood of `a`. In other words, if a Cauchy filter's sequence defined by controlled diameters converges to a point, then the filter is contained within the neighborhood of that point.
More concisely: Given a uniform space `(α, U)`, a Cauchy filter `f` on `α`, and a sequence `{U_n}` of sets in `U` such that for every `s` in `U` there exists an `n` with `U_n ⊆ s`, if there exists a point `a` in `α` such that the sequence `{x_n}` in `α` defined by `x_n ∈ U_n` converges to `a`, then `f ⊆ Nbd(a)`, where `Nbd(a)` denotes the neighborhood of `a`.
|
le_nhds_of_cauchy_adhp
theorem le_nhds_of_cauchy_adhp :
∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} {x : α}, Cauchy f → ClusterPt x f → f ≤ nhds x := by
sorry
This theorem states that if `x` is a cluster point (also known as an adherent point) for a Cauchy filter `f` in a uniform space `α`, then `x` is also a limit point for `f`. In other words, any Cauchy filter that has `x` as a cluster point is contained within the neighborhood of `x`. This implies that the values in the filter `f` get arbitrarily close to `x`, which is the definition of `x` being a limit point for the filter `f`.
More concisely: If a Cauchy filter `f` in a uniform space `α` has `x` as a cluster point, then `x` is a limit point of `f`.
|
IsCompact.totallyBounded
theorem IsCompact.totallyBounded :
∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α}, IsCompact s → TotallyBounded s
This theorem states that for any type `α` that has a uniform space structure and any set `s` of type `α`, if `s` is compact, then `s` is totally bounded. In other words, if every nontrivial filter that contains the set `s` has a cluster point in `s`, then for every entourage `d`, there exists a finite set `t` such that each element of `s` is `d`-near to some element of `t`. This theorem connects the concepts of compactness and total boundedness in a uniform space.
More concisely: In a uniform space, any compact set is totally bounded.
|