TopologicalSpace.denseRange_denseSeq
theorem TopologicalSpace.denseRange_denseSeq :
∀ (α : Type u) [t : TopologicalSpace α] [inst : TopologicalSpace.SeparableSpace α] [inst_1 : Nonempty α],
DenseRange (TopologicalSpace.denseSeq α)
This theorem states that for any non-empty type `α` that is equipped with a topology and is also separable, the sequence `TopologicalSpace.denseSeq α` has a dense range. In other words, the image of this sequence is a dense subset of `α`. In the context of topology, a set being "dense" in `α` means that every point of `α` is either in the set or is a limit point of the set, and a separable space is a space that contains a countable, dense subset.
More concisely: In a separable topological space `α`, the sequence `TopologicalSpace.denseSeq α` has a dense image.
|
TopologicalSpace.isBasis_countableBasis
theorem TopologicalSpace.isBasis_countableBasis :
∀ (α : Type u) [t : TopologicalSpace α] [inst : SecondCountableTopology α],
TopologicalSpace.IsTopologicalBasis (TopologicalSpace.countableBasis α)
The theorem `TopologicalSpace.isBasis_countableBasis` states that for all types `α` that have a topological space structure and a second countable topology, the countable basis defined for `α` is indeed a topological basis. In other words, the set of sets defined as the countable basis forms a topological basis for the topology on the type `α`. This is true for any space that has a second countable topology, which means that the topology has a countable basis.
More concisely: For any second countable topological space `α`, its countable basis is a topological basis.
|
Set.PairwiseDisjoint.countable_of_isOpen
theorem Set.PairwiseDisjoint.countable_of_isOpen :
∀ {α : Type u} [t : TopologicalSpace α] [inst : TopologicalSpace.SeparableSpace α] {ι : Type u_2} {s : ι → Set α}
{a : Set ι}, a.PairwiseDisjoint s → (∀ i ∈ a, IsOpen (s i)) → (∀ i ∈ a, (s i).Nonempty) → a.Countable
This theorem states that in a separable topological space, if there exists a family of nonempty open sets indexed by a set, and these open sets are pairwise disjoint, then the indexing set is countable. In other words, in a separable space, we can only have a countable number of nonempty open sets that do not intersect each other.
More concisely: In a separable topological space, if there exists a countable family of pairwise disjoint, nonempty open sets, then the space is second-countable.
|
TopologicalSpace.exists_countable_basis
theorem TopologicalSpace.exists_countable_basis :
∀ (α : Type u) [t : TopologicalSpace α] [inst : SecondCountableTopology α],
∃ b, b.Countable ∧ ∅ ∉ b ∧ TopologicalSpace.IsTopologicalBasis b
This theorem states that for any type `α` and any topological space `t` defined over `α`, if the topology is second-countable (i.e. it has a countable base), then there exists a basis `b` for this topological space such that `b` is a countable set, the empty set is not an element of `b`, and `b` forms a topological basis in the sense that every open set in the topological space can be written as a union of some elements of `b`.
More concisely: If `α` is a type and `t` is a second-countable topology on `α`, then there exists a countable, basis `b` for `t` that is a cover of the topology, i.e., every open set in `t` can be written as a union of some elements of `b`, with the empty set not being an element of `b`.
|
SecondCountableTopology.is_open_generated_countable
theorem SecondCountableTopology.is_open_generated_countable :
∀ {α : Type u} [t : TopologicalSpace α] [self : SecondCountableTopology α],
∃ b, b.Countable ∧ t = TopologicalSpace.generateFrom b
This theorem states that for any type `α` and a given topological space `t` on `α`, if `α` has a second-countable topology (indicated by `[self : SecondCountableTopology α]`), then there exists a countable set `b` of sets. In addition to being countable, this set `b` has the property that the topological space `t` is generated from `b` using the function `TopologicalSpace.generateFrom`. The function `TopologicalSpace.generateFrom` takes as input a collection of sets and outputs the smallest topological space that contains all the given sets. This theorem is part of the foundation for the theory of second-countable spaces, which are important in many areas of mathematics and specifically in topology.
More concisely: In a second-countable topological space `t` on type `α`, there exists a countable set `b` of sets generating `t` through `TopologicalSpace.generateFrom`.
|
TopologicalSpace.isTopologicalBasis_of_subbasis
theorem TopologicalSpace.isTopologicalBasis_of_subbasis :
∀ {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)},
t = TopologicalSpace.generateFrom s →
TopologicalSpace.IsTopologicalBasis ((fun f => f.sInter) '' {f | f.Finite ∧ f ⊆ s})
This theorem states that given a family of sets `s` that generates a topology `t` on a type `α`, the intersections of finite subcollections of `s` form a topological basis. In other words, if `t` equals the topology generated from `s`, then the image of the function that maps each set `f` to its intersection (where `f` is finite and a subset of `s`) forms a topological basis. This theorem is fundamental in the study of topological spaces in mathematics, particularly in understanding the structure and properties of topologies generated from a set of basis elements.
More concisely: Given a topology `t` on type `α` generated by a family of sets `s`, the intersections of finite subsets of `s` form a topological basis for `t`.
|
TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
theorem TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open :
∀ {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)},
TopologicalSpace.IsTopologicalBasis b → ∀ {a : α} {u : Set α}, a ∈ u → IsOpen u → ∃ v ∈ b, a ∈ v ∧ v ⊆ u
This theorem states that for any type `α` having a topology `t` and a set `b` of sets of `α` that forms a topological basis, for any member `a` of `α` and any open set `u` of `α` that contains `a`, there exists a set `v` in the basis `b` such that `a` is a member of `v` and `v` is a subset of `u`. In other words, given any topological space, any point in an open set of the space lies within some basis element contained within that open set.
More concisely: For any point in a topological space and open set containing it, there exists a basis element that contains the point and is a subset of the open set.
|
TopologicalSpace.IsTopologicalBasis.sUnion_eq
theorem TopologicalSpace.IsTopologicalBasis.sUnion_eq :
∀ {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)},
TopologicalSpace.IsTopologicalBasis s → s.sUnion = Set.univ
The theorem `TopologicalSpace.IsTopologicalBasis.sUnion_eq` states that for any given type `α` and any given topological space `t` on `α`, if you have a set `s` which is a topological basis of that space, the union of all the sets within `s` covers the entire space, i.e., it equals the universal set `Set.univ` of the type `α`. In other words, it's stating that a topological basis is a collection of sets whose union is the whole space.
More concisely: For any topological space `(α, t)` and topological basis `s` of `t` on `α`, the union of `s` equals the universal set `Set.univ` on `α`.
|
TopologicalSpace.FirstCountableTopology.tendsto_subseq
theorem TopologicalSpace.FirstCountableTopology.tendsto_subseq :
∀ {α : Type u} [t : TopologicalSpace α] [inst : FirstCountableTopology α] {u : ℕ → α} {x : α},
MapClusterPt x Filter.atTop u → ∃ ψ, StrictMono ψ ∧ Filter.Tendsto (u ∘ ψ) Filter.atTop (nhds x)
In a first-countable topological space, if a point `x` is a cluster point of a sequence `u` (meaning it's a point that every neighborhood of `x` contains infinitely many terms of the sequence `u`), then there exists a strictly monotone function `ψ` such that the composition of `u` and `ψ` tends to `x` (meaning for every neighborhood of `x`, the pre-image under the composed function eventually lies within that neighborhood) as we go to infinity. Essentially, we can re-index the sequence such that it converges to the cluster point `x`.
More concisely: In a first-countable topological space, every sequence with a cluster point `x` admits a strictly monotone reindexing whose limit is `x`.
|
TopologicalSpace.IsTopologicalBasis.continuous_iff
theorem TopologicalSpace.IsTopologicalBasis.continuous_iff :
∀ {α : Type u} [t : TopologicalSpace α] {β : Type u_2} [inst : TopologicalSpace β] {B : Set (Set β)},
TopologicalSpace.IsTopologicalBasis B → ∀ {f : α → β}, Continuous f ↔ ∀ s ∈ B, IsOpen (f ⁻¹' s)
The theorem `TopologicalSpace.IsTopologicalBasis.continuous_iff` states that for any types `α` and `β`, where `TopologicalSpace α` and `TopologicalSpace β` are instances, given a set `B` which is a topological basis of `β`, a function `f` from `α` to `β` is continuous if and only if for every set `s` in the basis `B`, the inverse image of `s` under `f` is an open set in `α`. In other words, a function between two topological spaces is continuous if it preserves the openness property of the basis sets of the target space.
More concisely: A function between two topological spaces is continuous if and only if the inverse image of every open set in the basis of the target space is an open set in the domain.
|
TopologicalSpace.IsTopologicalBasis.dense_iff
theorem TopologicalSpace.IsTopologicalBasis.dense_iff :
∀ {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)},
TopologicalSpace.IsTopologicalBasis b → ∀ {s : Set α}, Dense s ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty
This theorem states that a set in a topological space is dense if and only if it has non-empty intersection with all basis sets. More precisely, given a topological space `α` and a set `b` that forms a topological basis for `α`, for any set `s` in `α`, `s` is dense if it satisfies the property that for every basis set `o` in `b`, if `o` is non-empty then the intersection of `o` and `s` is also non-empty. In other words, a set is dense in a topological space if it intersects every open set from the topological basis non-trivially.
More concisely: A set in a topological space is dense if and only if it intersects non-emptily every open set in the topological basis.
|
TopologicalSpace.IsTopologicalBasis.sigma
theorem TopologicalSpace.IsTopologicalBasis.sigma :
∀ {ι : Type u_1} {E : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (E i)] {s : (i : ι) → Set (Set (E i))},
(∀ (i : ι), TopologicalSpace.IsTopologicalBasis (s i)) →
TopologicalSpace.IsTopologicalBasis (⋃ i, (fun u => Sigma.mk i '' u) '' s i)
The theorem `TopologicalSpace.IsTopologicalBasis.sigma` states that for any type `ι` and any type `E` indexed by `ι`, given a topological space structure on each `E i` and a set `s` of sets of each `E i` such that for each `i`, `s i` forms a topological basis for `E i`, then the union of the image of `s i` under the function that maps each set in `s i` to the set of pairs `(i, x)` where `x` is in the original set, forms a topological basis for the disjoint union space `Σ i, E i`. In other words, in a disjoint union space, a topological basis can be formed by taking the union of topological bases on each of the parts of the space.
More concisely: Given a family of topological spaces indexed by type `ι` with topological bases `s i` for each `E i`, the union of the images of `s i` under the canonical maps forms a topological basis for the disjoint union space `Σ i, E i`.
|
DenseRange.separableSpace
theorem DenseRange.separableSpace :
∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [inst : TopologicalSpace.SeparableSpace α]
[inst : TopologicalSpace β] {f : α → β}, DenseRange f → Continuous f → TopologicalSpace.SeparableSpace β
The theorem states that if `α` is a separable space and if there exists a continuous function `f` from `α` to `β` such that the range of `f` is dense in `β`, then `β` is also a separable space. In other words, the separability of a topological space is preserved under continuous maps with dense range. For example, the completion of a separable uniform space is also separable.
More concisely: If `α` is a separable topological space and `f: α → β` is a continuous function with a dense range, then `β` is separable.
|
TopologicalSpace.IsSeparable.of_separableSpace
theorem TopologicalSpace.IsSeparable.of_separableSpace :
∀ {α : Type u} [t : TopologicalSpace α] [h : TopologicalSpace.SeparableSpace α] (s : Set α),
TopologicalSpace.IsSeparable s
This theorem states that for any type `α` and a set `s` of this type, if `α` is equipped with a topology `t` and is a separable space (as denoted by `TopologicalSpace.SeparableSpace α`), then the set `s` is a separable set in the given topological space. In terms of topology, a separable space means that there exists a countable, dense subset within it. This result guarantees that any subset of such a space is also separable, i.e., it is contained within the closure of some countable set.
More concisely: In a separable topological space, every subset is separable.
|
Dense.exists_countable_dense_subset_bot_top
theorem Dense.exists_countable_dense_subset_bot_top :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : PartialOrder α] {s : Set α}
[inst_2 : TopologicalSpace.SeparableSpace ↑s],
Dense s →
∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
The theorem `Dense.exists_countable_dense_subset_bot_top` states that for any set `s` that is dense in a topological space `α` with a partial order structure, given that `s` is a separable space (for instance, when the topology of `α` is second countable), there exists a countable dense subset `t` of `s` with the properties that `t` contains the least (bottom) and the greatest (top) elements of `α` whenever these elements exist and are in `s`. For a dense subset that does not contain either the least or greatest elements, refer to `Dense.exists_countable_dense_subset_no_bot_top`.
More concisely: Given a dense, separable subset `s` of a partially ordered topological space `α`, there exists a countable dense subset `t` of `s` containing the least and greatest elements of `α` if they exist and are in `s`.
|
TopologicalSpace.isSeparable_range
theorem TopologicalSpace.isSeparable_range :
∀ {α : Type u} {β : Type u_1} [t : TopologicalSpace α] [inst : TopologicalSpace β]
[inst_1 : TopologicalSpace.SeparableSpace α] {f : α → β},
Continuous f → TopologicalSpace.IsSeparable (Set.range f)
The theorem `TopologicalSpace.isSeparable_range` states that for any two types `α` and `β` with `α` being a separable space in the context of topology, and any continuous function `f` from `α` to `β`, the range of `f` (i.e., the set of all outputs of `f`) is a separable set. Here, a set is said to be separable if it is contained in the closure of a countable set. The continuity of `f` ensures that the topological properties are preserved under the function mapping.
More concisely: For any separable space α and a continuous function f from α to a type β, the range of f is a separable set.
|
TopologicalSpace.IsTopologicalBasis.isOpen
theorem TopologicalSpace.IsTopologicalBasis.isOpen :
∀ {α : Type u} [t : TopologicalSpace α] {s : Set α} {b : Set (Set α)},
TopologicalSpace.IsTopologicalBasis b → s ∈ b → IsOpen s
This theorem states that for any type `α` with a given topology `t`, if `b` is a topological basis of the topological space, and `s` is a member of this basis `b`, then `s` is an open set in this topological space. In other words, this theorem asserts that every set in a topological basis is an open set in the corresponding topological space. This is a fundamental property of topological bases in topology.
More concisely: Given a topological space `(α, t)` and a topological basis `b ⊆ α`, every element `s ∈ b` is an open set in `α`.
|
TopologicalSpace.secondCountableTopology_induced
theorem TopologicalSpace.secondCountableTopology_induced :
∀ (α : Type u) (β : Type u_1) [t : TopologicalSpace β] [inst : SecondCountableTopology β] (f : α → β),
SecondCountableTopology α
This theorem states that if `β` is a second-countable space, then the topology induced on `α` via a function `f` from `α` to `β` is also second-countable. In other words, if you have a second-countable topological space, and you define a new topology on a different space using a function from that space to the second-countable one, the new topology is also second-countable. This holds for any types `α` and `β` and any function `f` from `α` to `β`.
More concisely: If `β` is a second-countable topological space and `f` is a function from a topological space `α` to `β`, then the topology on `α` induced by `f` is also second-countable.
|
TopologicalSpace.separableSpace_iff_countable
theorem TopologicalSpace.separableSpace_iff_countable :
∀ {α : Type u} [t : TopologicalSpace α] [inst : DiscreteTopology α],
TopologicalSpace.SeparableSpace α ↔ Countable α
This theorem states that for any type 'α' that comes equipped with a topological space structure and a discrete topology, this topological space is separable (i.e., contains a countable dense subset) if and only if the type 'α' itself is countable. The discrete topology on a set means that every subset is open, and separable refers to the existence of a countable dense subset.
More concisely: A type 'α' equipped with a discrete topology is separable if and only if 'α' is countable.
|
TopologicalSpace.exists_dense_seq
theorem TopologicalSpace.exists_dense_seq :
∀ (α : Type u) [t : TopologicalSpace α] [inst : TopologicalSpace.SeparableSpace α] [inst : Nonempty α],
∃ u, DenseRange u
This theorem states that for any nonempty separable topological space `α`, there exists a sequence `u` that has a dense range in `α`. In other words, it is always possible to find a sequence in `α` such that its range (or image) is a dense subset of `α`. The theorem suggests using `TopologicalSpace.denseSeq` and `TopologicalSpace.denseRange_denseSeq` instead of `cases` on its conclusion, and if `α` might be empty, `TopologicalSpace.exists_countable_dense` should be used.
In mathematical terms, a space is called separable if it contains a countable, dense subset. A set is called dense if every point of the space is either in the set or is a limit point of the set. A sequence is said to have a dense range if its image under some function forms a dense set.
More concisely: Every nonempty separable topological space has a dense sequence.
|
TopologicalSpace.IsTopologicalBasis.quotientMap
theorem TopologicalSpace.IsTopologicalBasis.quotientMap :
∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : TopologicalSpace Y] {π : X → Y}
{V : Set (Set X)},
TopologicalSpace.IsTopologicalBasis V →
QuotientMap π → IsOpenMap π → TopologicalSpace.IsTopologicalBasis (Set.image π '' V)
This theorem states that if we have a quotient map `π` from a topological space `X` to another topological space `Y`, and if `V` is a topological basis of `X`, then the image of `V` under `π` is a topological basis of `Y`. In other words, if a function `π` both is a quotient map and an open map, it preserves the property of being a topological basis when applied to sets of open sets in the domain topological space.
More concisely: If `π: X → Y` is a quotient map and an open map between topological spaces, and `V` is a topological basis for `X`, then the image `π[V]` is a topological basis for `Y`.
|
TopologicalSpace.IsTopologicalBasis.eq_generateFrom
theorem TopologicalSpace.IsTopologicalBasis.eq_generateFrom :
∀ {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)},
TopologicalSpace.IsTopologicalBasis s → t = TopologicalSpace.generateFrom s
This theorem states that for any type `α` and for any topological space `t` of type `α`, if `s` is a set of sets in `α` that forms a topological basis, then the topology `t` is the same as the topology generated by the basic sets `s`. In other words, the topology `t` is completely determined by its basic sets `s`.
More concisely: A topology on a type `α` is equal to the topology generated by any topological basis `s` of it.
|
TopologicalSpace.IsSeparable.of_subtype
theorem TopologicalSpace.IsSeparable.of_subtype :
∀ {α : Type u} [t : TopologicalSpace α] (s : Set α) [inst : TopologicalSpace.SeparableSpace ↑s],
TopologicalSpace.IsSeparable s
This theorem states that for any type `α` equipped with a topological space structure and any set `s` of `α`, if the subtype corresponding to `s` is a separable space, then `s` itself is a separable set in the topological space of `α`. In mathematics terms, this means that if we have a countable dense subset within the induced topology on `s`, then there exists a countable subset of `α` whose closure contains `s`.
More concisely: If `s` is a separable subspace of the topological space `α`, then `s` is a separable subset of `α`.
|
TopologicalSpace.IsTopologicalBasis.open_eq_sUnion'
theorem TopologicalSpace.IsTopologicalBasis.open_eq_sUnion' :
∀ {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)},
TopologicalSpace.IsTopologicalBasis B → ∀ {u : Set α}, IsOpen u → u = {s | s ∈ B ∧ s ⊆ u}.sUnion
This theorem states that for any type `α` and any topological space `t` on `α`, if `B` is a collection of sets that forms a topological basis of `t`, then any open set `u` in this topological space can be expressed as the union of basis sets that are contained in `u`. In other words, if we have a topological basis, every open set is just a union of these basic open sets.
More concisely: For any topological space `(α, t)` and topological basis `B` of `t`, every open set `u` in `t` can be written as a union of sets in `B` that are contained in `u`.
|
TopologicalSpace.countable_countableBasis
theorem TopologicalSpace.countable_countableBasis :
∀ (α : Type u) [t : TopologicalSpace α] [inst : SecondCountableTopology α],
(TopologicalSpace.countableBasis α).Countable
The theorem `TopologicalSpace.countable_countableBasis` states that for any type `α` and any given topological space `t` on `α` that has a second-countable topology (denoted by `inst`), the topological basis of `α` is countable. In other words, there exists an injective map from the set of basis elements to the set of natural numbers. This is essentially saying that in a second-countable topological space, the basis, which is the set of all possible open sets, can be listed in a sequence (or equivalently, enumerated), reflecting the property of second-countability.
More concisely: In a second-countable topological space, its topological basis is a countable set.
|
TopologicalSpace.IsSeparable.mono
theorem TopologicalSpace.IsSeparable.mono :
∀ {α : Type u} [t : TopologicalSpace α] {s u : Set α},
TopologicalSpace.IsSeparable s → u ⊆ s → TopologicalSpace.IsSeparable u
The theorem `TopologicalSpace.IsSeparable.mono` states that for any type `α` equipped with a topology `t` and any two sets `s` and `u` of `α`, if `s` is a separable set in the topological space and `u` is a subset of `s`, then `u` is also a separable set in the topological space. In other words, separability is a monotonic property: it is preserved under taking subsets.
More concisely: In a topological space, if a separable set is contained in another set, then the contained set is also separable.
|
FirstCountableTopology.nhds_generated_countable
theorem FirstCountableTopology.nhds_generated_countable :
∀ {α : Type u} [t : TopologicalSpace α] [self : FirstCountableTopology α] (a : α), (nhds a).IsCountablyGenerated
This theorem states that for any point `a` in a topological space `α`, if the topological space `α` has the property of being first countable (as indicated by `FirstCountableTopology α`), then the neighborhood filter at point `a`, denoted as `𝓝 a`, is countably generated. In other words, for any such topological space and point within it, there exists a countable collection of sets in the neighborhood filter of the point such that any set in the neighborhood filter can be represented as a union of some sub-collection of this countable set.
More concisely: In a first countable topological space, the neighborhood filter at any point is countably generated.
|
TopologicalSpace.IsTopologicalBasis.exists_subset_inter
theorem TopologicalSpace.IsTopologicalBasis.exists_subset_inter :
∀ {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)},
TopologicalSpace.IsTopologicalBasis s → ∀ t₁ ∈ s, ∀ t₂ ∈ s, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ s, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
For every topological space `α` and a set `s` of subsets of `α`, if `s` forms a topological basis, then for any two subsets `t₁` and `t₂` in `s` and any point `x` in the intersection of `t₁` and `t₂`, there exists a subset `t₃` in `s` such that `x` is in `t₃` and `t₃` is a subset of the intersection of `t₁` and `t₂`. This means that the set of all subsets `t` in `s` containing a given point `x` is directed downwards (i.e., for any two such subsets, there exists another one which is a subset of their intersection).
More concisely: Given a topological space `α` and a topological basis `s`, for any two basis elements `t₁` and `t₂` containing a point `x`, there exists a basis element `t₃` containing `x` that is a subset of both `t₁` and `t₂`.
|
QuotientMap.secondCountableTopology
theorem QuotientMap.secondCountableTopology :
∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : TopologicalSpace Y] {π : X → Y}
[inst_2 : SecondCountableTopology X], QuotientMap π → IsOpenMap π → SecondCountableTopology Y
The theorem `QuotientMap.secondCountableTopology` states that for any given types `X` and `Y` and topological spaces over them, if `X` is a second-countable topological space and a function `π : X → Y` is a quotient map and also an open map, then `Y` is also a second-countable topological space. In other words, under these conditions, the property of being a second-countable space is preserved under an open quotient map.
More concisely: If `π : X → Y` is an open quotient map between second-countable topological spaces `X` and `Y`, then `Y` is second-countable.
|
TopologicalSpace.isSeparable_univ_iff
theorem TopologicalSpace.isSeparable_univ_iff :
∀ {α : Type u} [t : TopologicalSpace α],
TopologicalSpace.IsSeparable Set.univ ↔ TopologicalSpace.SeparableSpace α
This theorem states that for any type `α` with a topological space structure `t`, the property of the universal set `Set.univ` (the set containing all elements of `α`) being separable is equivalent to the topological space `α` being separable. Here, a set is considered separable if it is contained in the closure of a countable set. Similarly, a topological space is called separable if there exists a countable dense subset. Thus, the theorem provides a characterization of separable topological spaces in terms of the separability of the universal set.
More concisely: A topological space is separable if and only if its universal set is separable as a set.
|
Set.Countable.isSeparable
theorem Set.Countable.isSeparable :
∀ {α : Type u} [t : TopologicalSpace α] {s : Set α}, s.Countable → TopologicalSpace.IsSeparable s
This theorem states that for any set `s` of a certain type `α` in a topological space `α`, if `s` is countable, then `s` is separable. In mathematical terms, if there exists an injective map from `s` to the set of natural numbers (denoting that `s` is countable), then there exists a countable set `c` whose closure contains `s` (denoting that `s` is separable in the topological space).
More concisely: If a countable set `s` in a topological space has an injective map to the natural numbers, then it is separable.
|
TopologicalSpace.SeparableSpace.of_denseRange
theorem TopologicalSpace.SeparableSpace.of_denseRange :
∀ {α : Type u} [t : TopologicalSpace α] {ι : Type u_2} [inst : Countable ι] (u : ι → α),
DenseRange u → TopologicalSpace.SeparableSpace α
The theorem `TopologicalSpace.SeparableSpace.of_denseRange` states that if a function `f`, denoted as `u` here, has a dense range and its domain is countable, then its codomain is a separable space. In other words, given a topological space `α`, and a function `u : ι → α` where `ι` is countable, if the range of `u` is dense in `α`, then `α` is a separable space. A separable space is a topological space that contains a countable dense subset. This theorem essentially provides a condition under which a space can be determined to be separable.
More concisely: A countable domain function with a dense range implies its codomain is a separable topological space.
|
DenseRange.separableSpace'
theorem DenseRange.separableSpace' :
∀ {α : Type u} [t : TopologicalSpace α] {ι : Type u_2} [inst : Countable ι] (u : ι → α),
DenseRange u → TopologicalSpace.SeparableSpace α
The theorem `DenseRange.separableSpace'` states that if a function `f`, represented here as `u` has a dense range, which means its range (or image) is a dense subset of `α`, and if its domain is countable (represented by the type `ι`), then the codomain `α` is a separable space in the topological sense. In other words, if we have a function whose values densely cover a topological space and the function's inputs are countable, then the topological space can be covered by a countable dense subset. This theorem is an alias of `TopologicalSpace.SeparableSpace.of_denseRange`.
More concisely: If a function with a dense range and countable domain maps to a topological space, then that space is separable.
|
TopologicalSpace.IsTopologicalBasis.nhds_hasBasis
theorem TopologicalSpace.IsTopologicalBasis.nhds_hasBasis :
∀ {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)},
TopologicalSpace.IsTopologicalBasis b → ∀ {a : α}, (nhds a).HasBasis (fun t => t ∈ b ∧ a ∈ t) fun t => t
This theorem states that for any type 'α' with a topology 't' and a set 'b' of subsets of 'α' which forms a topological basis, then for any element 'a' of 'α', the neighborhood filter of 'a' has a filter basis given by the set of those elements of 'b' which not only contain 'a' but are also themselves present in 'b'. In other words, it's ensuring that the neighborhood of any point in a topological space can be generated by sets from a topological basis that contain the given point.
More concisely: For any topological space ('α', 't'), and topological basis 'b' of 'α', the neighborhood filter of any point 'a' in 'α' has 'b' as a filter basis, i.e., the neighborhood filter of 'a' is the smallest filter containing all sets in 'b' that include 'a'.
|
exists_countable_dense_bot_top
theorem exists_countable_dense_bot_top :
∀ (α : Type u_1) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace.SeparableSpace α] [inst_2 : PartialOrder α],
∃ s, s.Countable ∧ Dense s ∧ (∀ (x : α), IsBot x → x ∈ s) ∧ ∀ (x : α), IsTop x → x ∈ s
The theorem `exists_countable_dense_bot_top` states that for any type `α` which is equipped with a topology and a separability condition, and also has a partial order, there exists a countable set `s` that is dense in `α`. Moreover, this set `s` contains any bottom element `x` (an element `x` is a bottom element if it is less than or equal to any other element in `α`) and any top element `x` (an element `x` is a top element if it is greater than or equal to any other element in `α`) in `α`, if they exist. For a dense set that does not contain either bottom or top elements, one may refer to the theorem `exists_countable_dense_no_bot_top`.
More concisely: For any separable topological space equipped with a partial order, there exists a countable dense set containing both the bottom and top elements, if they exist.
|
TopologicalSpace.IsSeparable.iUnion
theorem TopologicalSpace.IsSeparable.iUnion :
∀ {α : Type u} [t : TopologicalSpace α] {ι : Sort u_2} [inst : Countable ι] {s : ι → Set α},
(∀ (i : ι), TopologicalSpace.IsSeparable (s i)) → TopologicalSpace.IsSeparable (⋃ i, s i)
The theorem `TopologicalSpace.IsSeparable.iUnion` states that, for any type `α` that has a topological space structure, any countable index set `ι`, and any indexed collection of sets `s : ι → Set α` where each set `s i` is separable, the union of all these sets (`⋃ i, s i`) is also separable. In other words, if each set in a countable collection of sets is separable in a given topological space, then the union of all these sets is also separable in that topological space.
More concisely: If `α` is a topological space, `ι` is a countable index set, and each `s : ι → Set α` is a separable family of sets, then their union `⋃ i, s i` is separable in `α`.
|
TopologicalSpace.countable_cover_nhds
theorem TopologicalSpace.countable_cover_nhds :
∀ {α : Type u} [t : TopologicalSpace α] [inst : SecondCountableTopology α] {f : α → Set α},
(∀ (x : α), f x ∈ nhds x) → ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = Set.univ
This theorem states that in a topological space with a second-countable topology, given a function `f` that maps each point `x` to a neighborhood of `x`, there exists a countable set `s` such that the union of the neighborhoods `f x` for each `x` in `s` covers the entire space. This means that every point in the space is in the neighborhood `f x` for some `x` in `s`.
More concisely: In a second-countable topological space, given a function mapping each point to a neighborhood of it, there exists a countable set of points whose neighborhoods cover the entire space.
|
TopologicalSpace.IsSeparable.closure
theorem TopologicalSpace.IsSeparable.closure :
∀ {α : Type u} [t : TopologicalSpace α] {s : Set α},
TopologicalSpace.IsSeparable s → TopologicalSpace.IsSeparable (closure s)
This theorem states that for any set `s` in a topological space `α`, if `s` is a separable set, then the closure of `s` is also a separable set. Here, a set is called separable if it can be contained within the closure of some countable set. The closure of a set `s` is the smallest closed set that contains `s`.
More concisely: If a set `s` in a topological space is separable, then the closure of `s` is also a separable set.
|
TopologicalSpace.IsTopologicalBasis.quotient
theorem TopologicalSpace.IsTopologicalBasis.quotient :
∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Setoid X} {V : Set (Set X)},
TopologicalSpace.IsTopologicalBasis V →
IsOpenMap Quotient.mk' → TopologicalSpace.IsTopologicalBasis (Set.image Quotient.mk' '' V)
The theorem `TopologicalSpace.IsTopologicalBasis.quotient` states that for any type `X` with a topology, a setoid `S` on `X`, and a set `V` of subsets of `X`, if `V` forms a topological basis for the topology on `X` and `Quotient.mk'` is an open map from `X` to its quotient space by `S`, then the image of `V` under `Quotient.mk'` forms a topological basis for the quotient topology on the quotient space. In simple terms, if we have a basis for a topological space and we take the image of this basis under the quotient map, this image forms a basis for the topology on the quotient space. The quotient map here is `Quotient.mk'` which takes an element to its equivalence class under the setoid `S`.
More concisely: Given a topological space (X, top) with a topological basis V and quotient space (X/S, top') obtained by an open quotient map from X to X/S using a setoid S, then the image of V under the quotient map forms a topological basis for the quotient topology top' on X/S.
|
TopologicalSpace.IsTopologicalBasis.secondCountableTopology
theorem TopologicalSpace.IsTopologicalBasis.secondCountableTopology :
∀ {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)},
TopologicalSpace.IsTopologicalBasis b → b.Countable → SecondCountableTopology α
This theorem states that for any given type `α` and a topological space `t` over this type, if there exists a set `b` that forms a topological basis of the space, and this set `b` is countable (in the sense that there exists an injective map from `b` to the natural numbers), then the topology of the space is second-countable. In topological terms, a second-countable topology is one where there exists a countable base for the topology, that is, a countable collection of open sets such that every open set in the topology can be written as a union of sets from this collection.
More concisely: If `α` is a type with a countable topological basis `b`, then the topology on `α` is second-countable.
|
TopologicalSpace.exists_countable_dense
theorem TopologicalSpace.exists_countable_dense :
∀ (α : Type u) [t : TopologicalSpace α] [inst : TopologicalSpace.SeparableSpace α], ∃ s, s.Countable ∧ Dense s := by
sorry
This theorem states that for any type `α` equipped with a topological space structure and with the property that it is a separable space, there exists a set `s` that is both countable and dense in the topological space. In mathematical terms, this means that we can always find a countable set such that every point in the space belongs to the closure of this set. This theorem is a key result in topology, as it ensures the existence of a dense countable subset in any separable topological space.
More concisely: In any separable topological space, there exists a countable dense subset.
|
TopologicalSpace.SeparableSpace.exists_countable_dense
theorem TopologicalSpace.SeparableSpace.exists_countable_dense :
∀ {α : Type u} [t : TopologicalSpace α] [self : TopologicalSpace.SeparableSpace α], ∃ s, s.Countable ∧ Dense s := by
sorry
This theorem states that for any type `α` and given a topological space over `α`, if this topological space is separable, then there exists a set `s` that is both countable and dense in the topological space. In terms of mathematical language, we could say that in any separable topological space, we can always find a set that is countable (has the same cardinality as some subset of the natural numbers) and dense (every point in the space is in the closure of the set).
More concisely: In any separable topological space, there exists a countable, dense subset.
|
TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
theorem TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds :
∀ {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)},
(∀ u ∈ s, IsOpen u) →
(∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ s, a ∈ v ∧ v ⊆ u) → TopologicalSpace.IsTopologicalBasis s
The theorem states that for any type `α` equipped with a topology `t` and any set `s` of subsets of `α`, if all elements of `s` are open sets and for every element `a` of `α` and every open set `u` containing `a`, there exists a set `v` in `s` such that `a` is in `v` and `v` is a subset of `u`, then `s` is a topological basis.
In other words, a set of open sets forms a topological basis if and only if every open set can be written as a union of some collection of these sets. This is a fundamental concept in the study of topology, as it gives a way to construct and understand open sets.
More concisely: If a collection of open sets in a topological space has the property that every open set contains some set in the collection, then the collection forms a topological basis.
|
TopologicalSpace.IsTopologicalBasis.mem_nhds_iff
theorem TopologicalSpace.IsTopologicalBasis.mem_nhds_iff :
∀ {α : Type u} [t : TopologicalSpace α] {a : α} {s : Set α} {b : Set (Set α)},
TopologicalSpace.IsTopologicalBasis b → (s ∈ nhds a ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s)
This theorem states that in a given topological space `α`, a set `s` is in the neighborhood of an element `a` if and only if there exists some basis set `t` (from a collection `b` that forms a topological basis), such that `a` is contained in `t` and `t` itself is contained in `s`. In other words, `s` is a neighborhood of `a` precisely when `s` contains a basis set `t` that includes `a`. Here, a 'neighborhood' of `a` is defined as a set that contains an open set around `a`, and a 'topological basis' is a collection of sets whose union forms the topology and that intersects to form any given open set in the topology.
More concisely: A set is a neighborhood of an element in a topological space if and only if it contains a basis set that includes that element.
|
TopologicalSpace.IsSeparable.image
theorem TopologicalSpace.IsSeparable.image :
∀ {α : Type u} [t : TopologicalSpace α] {β : Type u_2} [inst : TopologicalSpace β] {s : Set α},
TopologicalSpace.IsSeparable s → ∀ {f : α → β}, Continuous f → TopologicalSpace.IsSeparable (f '' s)
The theorem `TopologicalSpace.IsSeparable.image` in Lean 4 states that, given a topological space `α`, another topological space `β`, a set `s` of elements of `α`, and a function `f` from `α` to `β` which is continuous, if the set `s` is separable in the topological space `α`, then the image of the set `s` under the function `f`, denoted by `f '' s`, is separable in the topological space `β`. Note that a set is called separable in a topological space if it is contained in the closure of a countable set.
More concisely: If `α` is a topological space, `β` is another topological space, `s ⊆ α` is separable, and `f : α → β` is a continuous function, then the image `f '' s` of `s` under `f` is separable in `β`.
|
Set.PairwiseDisjoint.countable_of_nonempty_interior
theorem Set.PairwiseDisjoint.countable_of_nonempty_interior :
∀ {α : Type u} [t : TopologicalSpace α] [inst : TopologicalSpace.SeparableSpace α] {ι : Type u_2} {s : ι → Set α}
{a : Set ι}, a.PairwiseDisjoint s → (∀ i ∈ a, (interior (s i)).Nonempty) → a.Countable
The theorem `Set.PairwiseDisjoint.countable_of_nonempty_interior` states that in a separable topological space, if we have a family of disjoint sets indexed by some set, each with a nonempty interior, then the indexing set must be countable. Here, a 'separable space' is a topological space that can be 'dense' in countably many points, 'pairwise disjoint' means any two distinct sets in the family have no element in common, and 'countable' means that there is a one-to-one correspondence between the set and the set of all natural numbers.
More concisely: In a separable topological space, a family of pairwise disjoint sets, each with a nonempty interior, has a countable indexing set.
|
TopologicalSpace.Quotient.secondCountableTopology
theorem TopologicalSpace.Quotient.secondCountableTopology :
∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Setoid X} [inst_1 : SecondCountableTopology X],
IsOpenMap Quotient.mk' → SecondCountableTopology (Quotient S)
This theorem states that if you have a second countable topological space `X` and an equivalence relation `S` on `X`, then if the canonical quotient map into a `Quotient` is an open map, the quotient space `Quotient S` is also a second countable topological space. In other words, an open quotient (using the quotient map on `X` that respects the equivalence relation `S`) of a second countable space is also second countable. This is an important property in topology that ensures the preservation of the second countability under the formation of quotient spaces by open maps.
More concisely: If `X` is a second countable topological space and `S` is an equivalence relation on `X` such that the quotient map is open, then the quotient space `Quotient S` is also second countable.
|
TopologicalSpace.isOpen_iUnion_countable
theorem TopologicalSpace.isOpen_iUnion_countable :
∀ {α : Type u} [t : TopologicalSpace α] [inst : SecondCountableTopology α] {ι : Type u_1} (s : ι → Set α),
(∀ (i : ι), IsOpen (s i)) → ∃ T, T.Countable ∧ ⋃ i ∈ T, s i = ⋃ i, s i
The theorem `TopologicalSpace.isOpen_iUnion_countable` states that for any type `α` that has a topology and a second-countable topology, given a set of open sets indexed by `ι`, if every one of these sets is open, there exists a countable subset `T` of `ι` such that the union of all the sets in `T` is equal to the union of all sets in `ι`. In other words, in a second-countable space, an open set that can be expressed as a union of open sets can also be represented as a union of countably many open sets. This implies that any open cover of `α` has a countable subcover, which characterizes `α` as a Lindelöf space (a topological space in which every open cover has a countable subcover).
More concisely: In a second-countable topological space, every open cover has a countable subcover.
|
TopologicalSpace.IsTopologicalBasis.sum
theorem TopologicalSpace.IsTopologicalBasis.sum :
∀ {α : Type u} {β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set (Set α)},
TopologicalSpace.IsTopologicalBasis s →
∀ {t : Set (Set β)},
TopologicalSpace.IsTopologicalBasis t →
TopologicalSpace.IsTopologicalBasis ((fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t)
This theorem states that given two topological spaces `α` and `β` and their respective topological bases `s` and `t`, a topological basis for the sum space `α ⊕ β` can be constructed by taking the union of the images of `s` and `t` under the left and right injection functions `Sum.inl` and `Sum.inr` respectively. Here, the sum space `α ⊕ β` is a type that includes all elements of the type `α` and all elements of the type `β`, and the left and right injection functions `Sum.inl` and `Sum.inr` are functions that take an element of `α` or `β` and return an element of `α ⊕ β`. The theorem asserts that the resulting set is indeed a topological basis for the sum space.
More concisely: The union of the images of topological bases `s` and `t` under the left and right injection functions `Sum.inl` and `Sum.inr`, respectively, forms a topological basis for the topological sum `α ⊕ β`.
|
TopologicalSpace.IsTopologicalBasis.mem_closure_iff
theorem TopologicalSpace.IsTopologicalBasis.mem_closure_iff :
∀ {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)},
TopologicalSpace.IsTopologicalBasis b →
∀ {s : Set α} {a : α}, a ∈ closure s ↔ ∀ o ∈ b, a ∈ o → (o ∩ s).Nonempty
This theorem states that for any type `α` and a topological space `t` over `α`, if `b` is a topological basis of the space, then for any set `s` of type `α` and any element `a` of `α`, `a` belongs to the closure of `s` if and only if every basis set `o` in `b` that contains `a` intersects with `s`. In mathematical terms, this means that any point `a` is in the closure of a set `s` if and only if all basis sets containing `a` have a non-empty intersection with `s`.
More concisely: A point `a` belongs to the closure of a set `s` in a topological space `t` if and only if for every topological basis element `o` in `t` containing `a`, `o` intersects `s` non-emptily.
|
TopologicalSpace.secondCountableTopology_of_countable_cover
theorem TopologicalSpace.secondCountableTopology_of_countable_cover :
∀ {α : Type u} [t : TopologicalSpace α] {ι : Sort u_1} [inst : Countable ι] {U : ι → Set α}
[inst : ∀ (i : ι), SecondCountableTopology ↑(U i)],
(∀ (i : ι), IsOpen (U i)) → ⋃ i, U i = Set.univ → SecondCountableTopology α
This theorem states that for every type `α` with a topology `t` and a countable indexing type `ι`, if for each index `i` in `ι` we have a set `U(i)` in `α` and the topology of `U(i)` is second-countable, and further, if each `U(i)` is an open set and the union of all `U(i)` is the universal set (i.e., covers all of `α`), then the topology on `α` is second-countable.
In terms of topology, this theorem provides a condition under which a topology is second countable: it is second countable if it can be covered by a countable collection of open sets, each of which is itself second countable.
In simple terms, a second-countable topology is one where we can find a countable basis, and this theorem says we can ensure a topology is second countable if we can cover it with a countable number of open sets that themselves have a countable basis.
More concisely: A topology on a countable indexing type `α` is second-countable if it can be generated by a countable base of second-countable open sets.
|
Inducing.secondCountableTopology
theorem Inducing.secondCountableTopology :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
[inst_2 : SecondCountableTopology β], Inducing f → SecondCountableTopology α
This theorem states that for any two types `α` and `β`, where `α` and `β` both have a topological space structure, and there is a function `f` from `α` to `β`. If `β` has a second countable topology, and `f` induces the topology of `α` from `β`, then `α` also has a second countable topology. Here, a second countable topology is one where there is a countable basis, and a function `f` is said to induce a topology when the topology on `α` is the coarsest one for which `f` is continuous.
More concisely: If `α` and `β` are topological spaces with `α` being second countable if and only if `β` is, and `f`: `α -> β` is a continuous function, then `α` has a second countable topology.
|