IsLindelof.disjoint_nhdsSet_left
theorem IsLindelof.disjoint_nhdsSet_left :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {l : Filter X} [inst_1 : CountableInterFilter l],
IsLindelof s → (Disjoint (nhdsSet s) l ↔ ∀ x ∈ s, Disjoint (nhds x) l)
This theorem states that for a Lindelöf set in a topological space, the neighborhood filter of the entire set is disjoint with a filter that has the countable intersection property if and only if, for each point in the set, its individual neighborhood filter is disjoint with this filter. Here, a set is considered Lindelöf if every nontrivial filter with the countable intersection property that contains the set has a cluster point in the set. Disjointness in this context means that the infimum of any two elements from the two entities (here, filters) is the bottom element. A neighborhood filter of a set or a point is the filter of all open sets containing the set or the point.
More concisely: A Lindelöf set in a topological space is disjoint with a filter having the countable intersection property if and only if the neighborhood filter of each point in the set is disjoint with that filter.
|
IsLindelof.compl_mem_sets
theorem IsLindelof.compl_mem_sets :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsLindelof s → ∀ {f : Filter X} [inst_1 : CountableInterFilter f], (∀ x ∈ s, sᶜ ∈ nhds x ⊓ f) → sᶜ ∈ f
The theorem `IsLindelof.compl_mem_sets` states that for any topological space `X` and any set `s` in `X`, if `s` is a Lindelöf set and `f` is a filter on `X` with the countable intersection property, then the complement of `s` belongs to the filter `f` if it belongs to the intersection of the neighborhood filter of every point `x` in `s` and the filter `f`. In other words, the complement of a Lindelöf set is in a given filter if it is in the local intersection of that filter for every point in the Lindelöf set.
More concisely: If a Lindelöf set in a topological space and a filter on the space with the countable intersection property, then the complement of the set belongs to the filter if it is in the local intersection of the filter at every point in the set.
|
Inducing.isLindelof_iff
theorem Inducing.isLindelof_iff :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
Inducing f → (IsLindelof s ↔ IsLindelof (f '' s))
The theorem states that for any types `X` and `Y` with respective topological spaces, any set `s` of type `X`, and any function `f` from `X` to `Y`, if `f` is an `Inducing` map (meaning that it induces the same topological structure on its image as the original set), then `s` is a Lindelöf set if and only if the image of `s` under `f` is a Lindelöf set. In other words, a set is Lindelöf (every nontrivial filter with the countable intersection property that contains the set has a cluster point in the set) if and only if its image under the inducing function is also Lindelöf.
More concisely: If `f` is a continuous function between topological spaces `X` and `Y` that induces the same topology on its image as `X`, then a set in `X` is Lindelöf if and only if its image under `f` is Lindelöf.
|
IsLindelof.elim_countable_subcover
theorem IsLindelof.elim_countable_subcover :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v},
IsLindelof s →
∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ r, r.Countable ∧ s ⊆ ⋃ i ∈ r, U i
The theorem `IsLindelöf.elim_countable_subcover` states that for any Lindelöf set `s` in a topological space `X` and any open cover `U` of `s`, there exists a countable subcover `r` of `U` such that `s` is a subset of the union over `r` of `U i`. This means if we have a Lindelöf set and an open cover, we can always find a countable subset of the cover that still covers the entire Lindelöf set. This is a fundamental property of Lindelöf spaces in topology.
More concisely: Given a Lindelöf set in a topological space and an open cover, there exists a countable subcover that still covers the set.
|
IsLindelof.image
theorem IsLindelof.image :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
IsLindelof s → Continuous f → IsLindelof (f '' s)
The theorem states that a continuous image of a Lindelöf set is also a Lindelöf set within the codomain. In more detail, given two types `X` and `Y`, both equipped with a topological space structure, a set `s` of type `X`, and a function `f` from `X` to `Y`, if `s` is a Lindelöf set and `f` is a continuous function, then the image of `s` under `f` (denoted as `f '' s`) is a Lindelöf set in `Y`. In the context of topology, a set is Lindelöf if every open cover has a countable subcover. This property is preserved under continuous mappings.
More concisely: A continuous image of a Lindelöf set is a Lindelöf set.
|
IsLindelof.inter_right
theorem IsLindelof.inter_right :
∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsLindelof s → IsClosed t → IsLindelof (s ∩ t)
The theorem states that the intersection of a Lindelöf set and a closed set is also a Lindelöf set. In more detail, given any type `X` that has a topological space structure and any two sets `s` and `t` of this type, if `s` is a Lindelöf set (meaning every nontrivial filter with the countable intersection property that contains `s` has a cluster point in `s`) and `t` is a closed set, then their intersection `(s ∩ t)` is also a Lindelöf set.
More concisely: If `s` is a Lindelöf set and `t` is a closed set in a topological space, then their intersection `s ∩ t` is also a Lindelöf set.
|
Set.Finite.isLindelof_biUnion
theorem Set.Finite.isLindelof_biUnion :
∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] {s : Set ι} {f : ι → Set X},
s.Finite → (∀ i ∈ s, IsLindelof (f i)) → IsLindelof (⋃ i ∈ s, f i)
This theorem states that for any type `X` equipped with a topological space structure, any set `s` of indices of type `ι`, and for any function `f` mapping indices to sets in `X`, if `s` is a finite set and every set `f(i)` is Lindelöf for each `i` in `s`, then the union of all `f(i)` for `i` in `s` is also a Lindelöf set. Recalling the definition, a Lindelöf set is one where each filter with the countable intersection property that contains the set has a cluster point in the set. So, the theorem essentially states a property about unions of Lindelöf sets in the context of a topological space.
More concisely: Given a topological space `X` and a finite set `s` of indices, if each `f(i)` is a Lindelöf set in `X` for every function `f` mapping indices to sets in `X`, then the union of all `f(i)` for `i` in `s` is also a Lindelöf set in `X`.
|
ClosedEmbedding.tendsto_coLindelof
theorem ClosedEmbedding.tendsto_coLindelof :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
ClosedEmbedding f → Filter.Tendsto f (Filter.coLindelof X) (Filter.coLindelof Y)
This theorem, `ClosedEmbedding.tendsto_coLindelof`, states the following: For any two types `X` and `Y`, each equipped with a topological space structure, and a function `f` from `X` to `Y`, if `f` is a closed embedding (which means it is a function that is both a homeomorphism onto its image and its image is a closed subset of `Y`), then `f` satisfies the property of `Filter.Tendsto` with respect to `Filter.coLindelof` of `X` and `Y`.
In other words, for every Lindelöf set in `Y` and its complement (which forms a neighborhood in the Lindelöf filter of `Y`), the preimage of this set under `f` is a neighborhood in the Lindelöf filter of `X`. This suggests that `f` preserves the structure of Lindelöf sets, mapping Lindelöf sets in `X` to Lindelöf sets in `Y`. Hence, the inverse images of Lindelöf sets are contained in Lindelöf sets, which signifies that closed embeddings are proper in the context of Lindelöf sets.
More concisely: A closed embedding between topological spaces preserves the property of being Lindelöf, i.e., the preimage of any Lindelöf set under a closed embedding is a Lindelöf set.
|
isLindelof_univ
theorem isLindelof_univ : ∀ {X : Type u} [inst : TopologicalSpace X] [h : LindelofSpace X], IsLindelof Set.univ := by
sorry
This theorem states that for any type `X` with a topological space structure and the Lindelof property, the universal set (which includes all elements of `X`) is a Lindelof set. In more mathematical terms, a space is said to be Lindelof if every open cover has a countable subcover. The Lindelof property is a weakening of compactness and is important in analysis and topology. Here, the theorem is basically asserting that if the whole space is Lindelof, then so is the universal set within that space.
More concisely: If `X` is a topological space with the Lindelof property, then the universal set of `X` also has the Lindelof property.
|
ClosedEmbedding.isLindelof_preimage
theorem ClosedEmbedding.isLindelof_preimage :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
ClosedEmbedding f → ∀ {K : Set Y}, IsLindelof K → IsLindelof (f ⁻¹' K)
This theorem states that the preimage of a Lindelöf set under a closed embedding is also a Lindelöf set. In more detail, given two types `X` and `Y` endowed with topological spaces, a function `f` from `X` to `Y`, and a set `K` in `Y` that is Lindelöf, if `f` is a closed embedding (a continuous function whose image is a closed set and has an inverse function on that image), then the preimage of `K` under `f` (i.e., the set of all elements in `X` that map to elements in `K` under `f`) is also a Lindelöf set. A Lindelöf set, remember, is one for which every nontrivial filter with the countable intersection property that contains the set, has a cluster point in the set.
More concisely: If `f : X ⟶ Y` is a closed embedding of topological spaces and `K ⊆ Y` is Lindelöf, then `f⁻¹(K) ⊆ X` is Lindelöf.
|
hasBasis_coLindelof
theorem hasBasis_coLindelof :
∀ {X : Type u} [inst : TopologicalSpace X], (Filter.coLindelof X).HasBasis IsLindelof compl
The theorem `hasBasis_coLindelof` states that for any type `X` equipped with a topological space structure, the filter `Filter.coLindelof X`, which is generated by the complements of Lindelöf sets, has a basis characterized by Lindelöf sets and their complements. In other words, each set in this filter can be generated by taking intersections of the complements of Lindelöf sets. A set is Lindelöf if every nontrivial filter with the property that it has countable intersections and contains the set, also has a cluster point in the set.
More concisely: The filter `Filter.coLindelof` on a topological space `X` is equal to the filter generated by the complements of Lindelöf sets.
|
nonLindelof_univ
theorem nonLindelof_univ :
∀ (X : Type u_2) [inst : TopologicalSpace X] [inst_1 : NonLindelofSpace X], ¬IsLindelof Set.univ
This theorem states that for any type `X` equipped with a topology (i.e. `X` is a topological space) and also having the property that it is a non-Lindelöf space (i.e., it does not meet the Lindelöf property), the universal set of `X` cannot be a Lindelöf set. In other words, if a topological space does not satisfy the Lindelöf condition (which requires that every open cover has a countable subcover), then its universal set, containing all its elements, also does not satisfy this condition.
More concisely: If a topological space `X` is non-Lindelöf, then its universal set is not Lindelöf.
|
IsLindelof.elim_nhds_subcover
theorem IsLindelof.elim_nhds_subcover :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsLindelof s →
∀ (U : X → Set X), (∀ x ∈ s, U x ∈ nhds x) → ∃ t, t.Countable ∧ (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
This theorem states that for any topological space `X` and any set `s` in `X`, if `s` is Lindelöf (i.e., every nontrivial filter with the countable intersection property that contains `s`, has a cluster point in `s`), then for any function `U` which maps each point `x` in `s` to a neighborhood of `x`, there exists a countable set `t` such that every element of `t` is in `s` and `s` is contained in the union of the neighborhoods `U x` for each `x` in `t`. In other words, if `s` has the property that every cover by open subsets has a countable subcover, then for any mapping of points in `s` to their neighborhoods, there is a countable subset of `s` whose associated neighborhoods cover `s`.
More concisely: If a subset `s` of a topological space `X` is Lindelöf, then for any function mapping each point in `s` to a neighborhood of that point, there exists a countable subset of `s` whose neighborhoods cover `s`.
|
LindelofSpace.of_continuous_surjective
theorem LindelofSpace.of_continuous_surjective :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
[inst_2 : LindelofSpace X], Continuous f → Function.Surjective f → LindelofSpace Y
The theorem `LindelofSpace.of_continuous_surjective` states that for any types `X` and `Y` equipped with topological spaces, if `f` is a continuous function from `X` to `Y` and it is surjective (i.e., for every element `y` in `Y`, there is an element `x` in `X` such that `f(x) = y`), then if `X` is a Lindelöf space, meaning that every open cover of `X` has a countable subcover, then `Y` is also a Lindelöf space. In other words, the continuous image of a Lindelöf space under a surjective function is also a Lindelöf space.
More concisely: If `X` is a Lindelöf space and `f: X → Y` is a continuous, surjective function, then `Y` is a Lindelöf space.
|
IsLindelof.elim_countable_subcover_image
theorem IsLindelof.elim_countable_subcover_image :
∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] {s : Set X} {b : Set ι} {c : ι → Set X},
IsLindelof s → (∀ i ∈ b, IsOpen (c i)) → s ⊆ ⋃ i ∈ b, c i → ∃ b' ⊆ b, b'.Countable ∧ s ⊆ ⋃ i ∈ b', c i
This theorem states that for any Lindelöf set 's' in a topological space, if it is covered by an open cover, there exists a countable subcover. More specifically, if 's' is a set in a topological space 'X', 'b' is a set of indices, and 'c' is a function from indices to sets in 'X' such that every 'c i' for 'i' in 'b' is open and the union of 'c i' for 'i' in 'b' covers 's', then there exists a countable subset 'b'' of 'b' such that the union of 'c i' for 'i' in 'b'' also covers 's'. In other words, we can always find a countable collection of open sets from the original cover that still cover the entire Lindelöf set.
More concisely: A Lindelöf set in a topological space can be covered by a countable subcollection of open sets from any open cover.
|
isLindelof_iff_countable_subfamily_closed
theorem isLindelof_iff_countable_subfamily_closed :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsLindelof s ↔
∀ {ι : Type u} (t : ι → Set X),
(∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
The theorem `isLindelof_iff_countable_subfamily_closed` states that, for any given type `X` with a topological space structure and a set `s` of type `X`, the set `s` is Lindelöf if and only if the following condition holds: for any family of closed sets (indexed by any type `ι`) whose intersection does not include any elements of `s`, there exists a countable subfamily of this family of closed sets, whose intersection also does not include any elements of `s`.
In other words, the theorem connects the property of a set being Lindelöf in a topological space with the existence of countable subfamilies of closed sets which avoid the set. This property is of interest in topology as it is related to the compactness of the set.
More concisely: A set in a topological space is Lindelöf if and only if for any family of closed sets whose intersection does not contain the set, there exists a countable subfamily with the same property.
|
Filter.comap_coLindelof_le
theorem Filter.comap_coLindelof_le :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
Continuous f → Filter.comap f (Filter.coLindelof Y) ≤ Filter.coLindelof X
This theorem states that for any two types `X` and `Y` with topological space structures and a continuous function `f` from `X` to `Y`, the filter obtained by comapping the coLindelöf filter on `Y` by `f` is less than or equal to the coLindelöf filter on `X`. It is a reformulation of the fact that the images of Lindelöf sets under a continuous function are also Lindelöf. A Lindelöf set is a topological space where every open cover has a countable subcover. The coLindelöf filter on a type is defined as the infimum over all complements of Lindelöf sets in the space.
More concisely: For any continuous function between two topological spaces and the coLindelöf filters on each, the image filter is less than or equal to the original coLindelöf filter.
|
IsLindelof.compl_mem_sets_of_nhdsWithin
theorem IsLindelof.compl_mem_sets_of_nhdsWithin :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsLindelof s →
∀ {f : Filter X} [inst_1 : CountableInterFilter f], (∀ x ∈ s, ∃ t ∈ nhdsWithin x s, tᶜ ∈ f) → sᶜ ∈ f
This theorem states that for any given type `X` with a topological space structure, and a set `s` of this type, if `s` is a Lindelöf set (i.e every nontrivial filter `f` with the countable intersection property that contains `s`, has a cluster point in `s`), then for any filter `f` with the countable intersection property, if every point `x` in `s` has a neighborhood `t` within `s` such that the complement of `t` belongs to `f`, then the complement of `s` belongs to `f`.
Essentially, the theorem connects the properties of Lindelöf sets (sets for which every open cover has a countable subcover), filters (a generalization of the concept of "small neighborhoods of a point"), and the concept of a neighborhood within a set in the context of topological spaces.
More concisely: If `X` is a topological space, `s` is a Lindelöf subset of `X`, and for every `x` in `s`, there exists a neighborhood `t` of `x` in `s` with complement in `s` belonging to the filter `f`, then the complement of `s` belongs to `f`.
|
IsLindelof.diff
theorem IsLindelof.diff :
∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsLindelof s → IsOpen t → IsLindelof (s \ t)
This theorem states that for any type `X` with an associated topological space, if `s` is a Lindelöf set and `t` is an open set, then the set difference `s \ t` (i.e., the set of all elements in `s` that are not in `t`) is also a Lindelöf set.
In other words, removing an open set from a Lindelöf set still results in a Lindelöf set. A Lindelöf set, in this context, is defined as a set such that every nontrivial filter on the set with the countable intersection property has a cluster point in the set.
More concisely: If `s` is a Lindelöf set and `t` is an open set in a topological space, then the set difference `s \ t` is also a Lindelöf set.
|
IsLindelof.inter_left
theorem IsLindelof.inter_left :
∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsLindelof t → IsClosed s → IsLindelof (s ∩ t)
The theorem states that for any type `X` equipped with a topology, if `t` is a Lindelöf set and `s` is a closed set, then the intersection of `s` and `t` is also a Lindelöf set. In other words, if every nontrivial filter with the countable intersection property that contains `t` has a cluster point in `t`, and `s` is a set that contains all its limit points, then every nontrivial filter with the countable intersection property that contains the intersection of `s` and `t` has a cluster point in the intersection of `s` and `t`.
More concisely: If `X` is a topological space, `t` is a Lindelöf set, and `s` is a closed set, then the intersection of `s` and `t` is also a Lindelöf set.
|
IsLindelof.compl_mem_coLindelof
theorem IsLindelof.compl_mem_coLindelof :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsLindelof s → sᶜ ∈ Filter.coLindelof X
The theorem `IsLindelof.compl_mem_coLindelof` states that for any type `X` equipped with a topological space structure and any set `s` of type `X`, if `s` is a Lindelöf set (meaning that every nontrivial filter `f` with the countable intersection property that contains `s`, has a cluster point in `s`), then the complement of `s` is a member of the coLindelöf filter of `X`. The coLindelöf filter of `X` is defined as the filter generated by complements of all Lindelöf sets in `X`.
More concisely: If a set `s` in a topological space `X` is Lindelöf, then the complement of `s` belongs to the filter generated by the complements of all Lindelöf sets in `X`.
|
IsLindelof.of_isClosed_subset
theorem IsLindelof.of_isClosed_subset :
∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsLindelof s → IsClosed t → t ⊆ s → IsLindelof t := by
sorry
This theorem states that a closed subset of a Lindelöf set is also a Lindelöf set. In detail, given any type `X` that is equipped with a topology, and any two sets `s` and `t` of this type, if `s` is a Lindelöf set, `t` is a closed set and `t` is a subset of `s`, then `t` is also a Lindelöf set.
In the context of topology, a Lindelöf set is one where every open cover has a countable subcover. In this case, the theorem is stating that if we have a subset that is closed and is contained within a Lindelöf set, this subset is also Lindelöf. This is important as it ensures the Lindelöf property, which is often associated with compactness, is preserved under taking closed subsets.
More concisely: If a Lindelöf set contains a closed subset, then the closed subset is also Lindelöf.
|
Set.Countable.isLindelof_biUnion
theorem Set.Countable.isLindelof_biUnion :
∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] {s : Set ι} {f : ι → Set X},
s.Countable → (∀ i ∈ s, IsLindelof (f i)) → IsLindelof (⋃ i ∈ s, f i)
The theorem `Set.Countable.isLindelof_biUnion` states that, given a topological space `X`, a countable set `s` of indices of type `ι`, and a function `f` mapping indices to subsets of `X`, if each of the subsets `f i` for `i` in `s` is a Lindelöf space, then the union of these subsets (i.e., ⋃ {i ∈ s, f i}) is also a Lindelöf space. In other words, a countable union of Lindelöf spaces is itself a Lindelöf space. A Lindelöf space, as defined here, is a topological space in which every nontrivial filter with the countable intersection property that contains the set has a cluster point in the set.
More concisely: A countable union of Lindelöf spaces is a Lindelöf space.
|
isLindelof_range
theorem isLindelof_range :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : LindelofSpace X]
{f : X → Y}, Continuous f → IsLindelof (Set.range f)
The theorem `isLindelof_range` states that for any two types `X` and `Y`, given `X` has a topological space structure and `Y` also has a topological space structure, and if `X` is a Lindelöf space, then for any continuous function `f` from `X` to `Y`, the range of `f` is also a Lindelöf set.
In other words, if we have a continuous function mapping from a Lindelöf space to any other topological space, then the set of all possible outcomes of this function will always retain the Lindelöf property, i.e., every nontrivial filter with the countable intersection property that contains this range set has a cluster point in this range set.
More concisely: If `X` is a Lindelöf topological space and `f : X -> Y` is a continuous function with `Y` being any topological space, then the range of `f` is a Lindelöf subset of `Y`.
|
isLindelof_empty
theorem isLindelof_empty : ∀ {X : Type u} [inst : TopologicalSpace X], IsLindelof ∅
This theorem states that the empty set is a Lindelöf set. In more detail, for any type `X` and any topological space on `X`, the empty set satisfies the Lindelöf property. This means that for any nontrivial filter `f` with the countable intersection property, if `f` is included in the principal filter generated by the empty set, then there exists a cluster point in the empty set. However, since the empty set has no elements, the condition on the filter `f` is automatically unsatisfiable, and hence the empty set trivially satisfies the Lindelöf property.
More concisely: The empty set is a Lindelöf set in any topological space, as its only filter satisfying the countable intersection property is the trivial filter, which has no elements.
|
isLindelof_of_countable_subfamily_closed
theorem isLindelof_of_countable_subfamily_closed :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
(∀ {ι : Type u} (t : ι → Set X),
(∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅) →
IsLindelof s
The theorem `isLindelof_of_countable_subfamily_closed` states that for any set `s` in a topological space `X`, `s` is Lindelöf if for each family of closed sets, indexed by a type `ι`, whose intersection does not intersect `s`, there exists a countable subfamily of this family of closed sets whose intersection also does not intersect `s`. In this context, a set `s` being Lindelöf means that any non-trivial filter `f` with the countable intersection property, that contains `s`, has a cluster point in `s`. A filter `f` having the countable intersection property means that the intersection of any countable collection of sets from `f` is also in `f`.
More concisely: A set `s` in a topological space is Lindelöf if for every family of closed sets whose intersection does not intersect `s`, there exists a countable subfamily whose intersection also does not intersect `s`.
|
IsLindelof.disjoint_nhdsSet_right
theorem IsLindelof.disjoint_nhdsSet_right :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {l : Filter X} [inst_1 : CountableInterFilter l],
IsLindelof s → (Disjoint l (nhdsSet s) ↔ ∀ x ∈ s, Disjoint l (nhds x))
The theorem `IsLindelof.disjoint_nhdsSet_right` states that for a given type `X` equipped with a topological space structure, a set `s` of `X`, and a filter `l` on `X` with the countable intersection property, if `s` is a Lindelöf set, then `l` being disjoint with the filter of neighborhoods of `s` is equivalent to `l` being disjoint with the neighborhood filter of each point in `s`. Here, a Lindelöf set is a set in which every nontrivial filter with the countable intersection property that contains the set has a cluster point in the set. Two elements are considered disjoint if their infimum is the bottom element. The neighborhood filter of a set is the supremum of the filters of neighborhoods of each point in the set, and the neighborhood filter of a point is the infimum over the principal filters of all open sets containing the point.
More concisely: For a Lindelöf set `s` in a topological space `X` and a filter `l` on `X` with the countable intersection property, `l` is disjoint with the filter of neighborhoods of `s` if and only if it is disjoint with the neighborhood filters of all points in `s`.
|
isLindelof_iff_countable_subcover
theorem isLindelof_iff_countable_subcover :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsLindelof s ↔
∀ {ι : Type u} (U : ι → Set X),
(∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i
The theorem `isLindelof_iff_countable_subcover` states that a set `s` is Lindelöf if and only if for each open cover of `s`, there exists a countable subcover. In other words, for any topological space `X` and any set `s` in that space, `s` is Lindelöf precisely when every function `U` from an arbitrary type `ι` to the set `X`, such that every `U i` is an open set, and `s` is a subset of the union of all `U i`, there exists a set `t` which is countable and `s` is a subset of the union of `U i` for every `i` in `t`. This links the notion of a Lindelof set to the existence of countable subcovers of open coverings.
More concisely: A set in a topological space is Lindelöf if and only if it has a countable subcover for every open cover.
|
IsLindelof.elim_countable_subfamily_closed
theorem IsLindelof.elim_countable_subfamily_closed :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v},
IsLindelof s →
∀ (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, u.Countable ∧ s ∩ ⋂ i ∈ u, t i = ∅
The theorem states that for any topological space `X` and any subset `s` of `X` that has the Lindelöf property, for every family of closed subsets of `X`, if the intersection of `s` and the intersection of the entire family is empty, then there exists a countable subfamily such that the intersection of `s` and the intersection of the subfamily is also empty. In other words, if a Lindelöf set avoids the intersection of an entire family of closed sets, then it can also avoid the intersection of a countable subfamily of those sets.
More concisely: If `X` is a topological space and `s` is a Lindelöf subset of `X` that avoids the intersection of every countable family of closed subsets of `X`, then it avoids the intersection of some countable subfamily.
|
LindelofSpace.isLindelof_univ
theorem LindelofSpace.isLindelof_univ :
∀ {X : Type u_2} [inst : TopologicalSpace X] [self : LindelofSpace X], IsLindelof Set.univ
This theorem states that in a Lindelöf space, the universal set is a Lindelöf set. More specifically, for any topological space that is a Lindelöf space, every nontrivial filter with the countable intersection property that contains the entire space, has a cluster point in the space. In other words, if we take all possible points in the topological space (i.e., the universal set), this set has the property that any countable collection of open sets that cover the space can be reduced to a countable subcover.
More concisely: In a Lindelöf space, the universal set has the property of being a Lindelöf collection, meaning any countable open cover has a countable subcover.
|
IsLindelof.union
theorem IsLindelof.union :
∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsLindelof s → IsLindelof t → IsLindelof (s ∪ t) := by
sorry
The theorem `IsLindelof.union` states that for any type `X` with a topological space structure and any two sets `s` and `t` of type `X`, if both `s` and `t` are Lindelöf sets, then their union `s ∪ t` is also a Lindelöf set. In other words, in a topological space, the union of two Lindelöf sets is still a Lindelöf set. Here, a set is Lindelöf if every non-trivial filter with the countable intersection property that contains the set, has a cluster point within the set.
More concisely: In a topological space, the union of two Lindelöf sets is a Lindelöf set.
|
IsLindelof.image_of_continuousOn
theorem IsLindelof.image_of_continuousOn :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
IsLindelof s → ContinuousOn f s → IsLindelof (f '' s)
This theorem states that if a set `s` in a topological space `X` is Lindelöf, and there is a function `f` from `X` to another topological space `Y` which is continuous on `s`, then the image of `s` under `f`, denoted as `f '' s`, is also a Lindelöf set in `Y`.
In other words, the Lindelöf property is preserved under continuous mappings. The Lindelöf property for a set is defined as: for any nontrivial filter with the countable intersection property that contains the set, there exists a cluster point in the set. A function is continuous on a set if it is continuous at every point in the set.
More concisely: If `s` is a Lindelöf set in a topological space `X` and `f : X → Y` is a continuous function, then `f '' s` is a Lindelöf set in `Y`.
|
HereditarilyLindelofSpace.isHereditarilyLindelof_univ
theorem HereditarilyLindelofSpace.isHereditarilyLindelof_univ :
∀ {X : Type u_2} [inst : TopologicalSpace X] [self : HereditarilyLindelofSpace X],
IsHereditarilyLindelof Set.univ
This theorem states that in a Hereditarily Lindelöf space (a topological space in which every subset is a Lindelöf set), the universal set (the set containing all elements) is itself a Hereditarily Lindelöf set. More precisely, for any type `X` equipped with a topological structure, if `X` forms a Hereditarily Lindelöf space, then the universal set in `X` inherits this property, meaning that every subset of the universal set is also a Lindelöf set.
More concisely: In a Hereditarily Lindelöf space, the universal set is also a Hereditarily Lindelöf set. Every subset is a Lindelöf set.
|
IsLindelof.adherence_nhdset
theorem IsLindelof.adherence_nhdset :
∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X} {f : Filter X} [inst_1 : CountableInterFilter f],
IsLindelof s → f ≤ Filter.principal s → IsOpen t → (∀ x ∈ s, ClusterPt x f → x ∈ t) → t ∈ f
The theorem `IsLindelof.adherence_nhdset` states that for any type `X` with a topological space structure, given sets `s` and `t` in `X`, and a filter `f` on `X` with the countable intersection property, if `s` is a Lindelöf set, `f` is finer than the principal filter on `s`, and `t` is an open set that contains all cluster points of `s` with respect to `f`, then `t` is in the filter `f`. In simpler words, it says that any open set that contains all cluster points of a Lindelöf set `s`, under a filter `f` with countable intersection property and finer than principal filter on `s`, belongs to the filter `f`.
More concisely: If `X` is a topological space, `s` is a Lindelöf subset of `X`, `f` is a countably intersecting filter on `X` finer than the principal filter on `s`, and `t` is an open set containing all cluster points of `s` with respect to `f`, then `t` is in `f`.
|
isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis
theorem isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis :
∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] (b : ι → Set X),
TopologicalSpace.IsTopologicalBasis (Set.range b) →
(∀ (i : ι), IsLindelof (b i)) → ∀ (U : Set X), IsLindelof U ∧ IsOpen U ↔ ∃ s, s.Countable ∧ U = ⋃ i ∈ s, b i
This theorem states that for a topological space `X` and a basis `b` consisting of sets `b i` where each `b i` is Lindelöf, an open set `U` in `X` is Lindelöf if and only if it can be expressed as a countable union of some elements in the basis. Here, `TopologicalSpace.IsTopologicalBasis (Set.range b)` means that the range of `b` forms a topological basis for the space `X`, and `IsLindelof U` implies that `U` is a Lindelöf set, i.e., every nontrivial filter with the countable intersection property that contains `U`, has a cluster point in `U`. Similarly, `IsOpen U` indicates that `U` is an open set in `X`. The statement `∃ s, s.Countable ∧ U = ⋃ i ∈ s, b i` implies that there exists a countable set `s` such that `U` is equal to the union of sets `b i` over all `i` in `s`.
More concisely: A topological space endowed with a countable, Lindelöf basis is Lindelöf if and only if every open set can be expressed as a countable union of sets in the basis.
|
isLindelof_of_countable_subcover
theorem isLindelof_of_countable_subcover :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
(∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ t, t.Countable ∧ s ⊆ ⋃ i ∈ t, U i) →
IsLindelof s
The theorem `isLindelof_of_countable_subcover` asserts that a set `s` is Lindelöf in a given topological space `X` if, for any open cover of `s` (denoted by `(U : ι → Set X)`, where each `U i` is an open set), there exists a countable subcover. This means that if we can cover `s` using an arbitrary index set `ι` of open sets, and `s` is a subset of the union of these open sets, then there exists a countable index set `t` such that `s` is still a subset of the union of the open sets indexed by `t`. Essentially, this theorem provides a condition under which a set is Lindelöf: it is Lindelöf if we can always find a countable subcover of any open cover.
More concisely: A set is Lindelöf in a topological space if every open cover of the set has a countable subcover.
|
NonLindelofSpace.nonLindelof_univ
theorem NonLindelofSpace.nonLindelof_univ :
∀ {X : Type u_2} [inst : TopologicalSpace X] [self : NonLindelofSpace X], ¬IsLindelof Set.univ
The theorem `NonLindelofSpace.nonLindelof_univ` states that in a non-Lindelöf space, the universal set, which contains all elements of the space, is not a Lindelöf set. In other words, for any type `X` equipped with a topological space structure and happens to be non-Lindelöf, the universal set in `X` does not satisfy the Lindelöf property. The Lindelöf property is defined such that every nontrivial filter with the countable intersection property that contains the set, has a cluster point in the set.
More concisely: In a non-Lindelöf topological space, the universal set does not have the Lindelöf property.
|
Inducing.isLindelof_preimage
theorem Inducing.isLindelof_preimage :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
Inducing f → IsClosed (Set.range f) → ∀ {K : Set Y}, IsLindelof K → IsLindelof (f ⁻¹' K)
The theorem `Inducing.isLindelof_preimage` states that if we have an inducing function from a topological space `X` to another topological space `Y`, and the range of this function is closed, then the preimage of any Lindelöf set in `Y` under this function is also a Lindelöf set in `X`. Here, a Lindelöf set is a set where every nontrivial filter that contains the set and has the countable intersection property has a cluster point in the set. An inducing function is a function that induces the topology of the codomain onto its domain.
More concisely: If `f` is an inducing function from a topological space `X` to a closed image in another topological space `Y`, and `S ⊆ Y` is Lindelöf, then `f⁻¹[S]` is Lindelöf in `X`.
|
IsLindelof.inter_iInter_nonempty
theorem IsLindelof.inter_iInter_nonempty :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v},
IsLindelof s →
∀ (t : ι → Set X),
(∀ (i : ι), IsClosed (t i)) →
(∀ (u : Set ι), u.Countable ∧ (s ∩ ⋂ i ∈ u, t i).Nonempty) → (s ∩ ⋂ i, t i).Nonempty
This theorem states that for a Lindelöf set within a topological space, if it intersects with every countable subfamily of a family of closed sets, it will also intersect with the intersection of the entire family of closed sets. More formally, if we have a set `s` that is Lindelöf in a topological space `X`, and a family of closed sets `t` indexed by `ι`, then if for every countable subset `u` of `ι`, the intersection of `s` with the intersection of the `t` sets indexed by `u` is nonempty, it implies that the intersection of `s` with the intersection of all `t` sets is nonempty. This theorem illustrates one of the properties that Lindelöf sets possess in topological spaces.
More concisely: A Lindelöf set in a topological space intersects the intersection of every countable family of closed sets if and only if it intersects their intersection.
|
IsLindelof.induction_on
theorem IsLindelof.induction_on :
∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
IsLindelof s →
∀ {p : Set X → Prop},
(∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s) →
(∀ (S : Set (Set X)), S.Countable → (∀ s ∈ S, p s) → p S.sUnion) →
(∀ x ∈ s, ∃ t ∈ nhdsWithin x s, p t) → p s
The theorem states that for any topological space `X` and any Lindelöf set `s` of `X`, if a property `p` holds for all sets that are the intersection of `s` and some neighbourhood of each point `x` in `s`, and `p` is stable under restriction (meaning if `p` holds for a set `t` and `s` is a subset of `t`, then `p` also holds for `s`) and union (meaning that if `p` holds for all sets in a countable collection `S` of sets, then `p` also holds for the union of `S`), then `p` also holds for the set `s`. In mathematical terms, this theorem is about the property of sets in a Lindelöf space related to topology, under certain stability conditions. This theorem could be used for proving properties about the Lindelöf spaces in the field of topology.
More concisely: In a Lindelöf space, if a property stable under restriction and union holds for the intersection of a Lindelöf set and every neighborhood of each point, then the property holds for the Lindelóf set itself.
|
IsCompact.isLindelof
theorem IsCompact.isLindelof : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsCompact s → IsLindelof s := by
sorry
The theorem `IsCompact.isLindelof` states that if a set `s` in a topological space `X` is compact, then it is also Lindelöf. In other words, for a set `s` to be compact means that for every nontrivial filter `f` that contains `s`, there exists an element `a` in `s` such that every set of `f` meets every neighborhood of `a`. If this condition is met, then the set `s` is also Lindelöf, meaning that every nontrivial filter `f` with the countable intersection property that contains `s`, has a cluster point in `s`.
More concisely: A compact set in a topological space is Lindelöf. In other words, every compact set has the property that every countable intersection of open sets with the set contains a point that is a limit point of the set.
|
isLindelof_singleton
theorem isLindelof_singleton : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X}, IsLindelof {x}
The theorem states that a singleton set is always a Lindelöf set. More specifically, for any type `X` equipped with a topological space structure and for any element `x` of `X`, the singleton set consisting of just `x` satisfies the property of being Lindelöf. This means that if we take any non-trivial filter `f` with a countable intersection property that contains the singleton set `{x}`, there always exists a cluster point in the set `{x}`.
More concisely: For any topological space `(X, top)` and element `x` in `X`, the singleton set `{x}` is a Lindelöf space.
|
isLindelof_iUnion
theorem isLindelof_iUnion :
∀ {X : Type u} [inst : TopologicalSpace X] {ι : Sort u_2} {f : ι → Set X} [inst_1 : Countable ι],
(∀ (i : ι), IsLindelof (f i)) → IsLindelof (⋃ i, f i)
The theorem `isLindelof_iUnion` states that for any type `X` with a topological space structure, and for any countable index set `ι`, if for each index `i` in `ι`, the set `f i` (a function from `ι` to the set of `X`) is Lindelöf, then the union of all the sets `f i` (denoted by `(⋃ i, f i)`) is also Lindelöf. A Lindelöf set in this context is one where every nontrivial filter (a "description" of a point's neighborhood) that has the countable intersection property and contains the set has a cluster point (a point in the closure of every neighborhood of the filter) in the set.
More concisely: If each set in a countable family of Lindelöf subsets of a topological space is Lindelöf, then their union is also a Lindelöf subset.
|
Embedding.isLindelof_iff
theorem Embedding.isLindelof_iff :
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {f : X → Y},
Embedding f → (IsLindelof s ↔ IsLindelof (f '' s))
The theorem states that for any two types `X` and `Y` having a topological structure, a set `s` of type `X`, and a function `f` from `X` to `Y`, if `f` is an embedding, then the set `s` is Lindelöf if and only if the image of set `s` under function `f` is Lindelöf. Here, a set being Lindelöf means that every nontrivial filter with the countable intersection property that contains the set, has a cluster point in the set.
More concisely: If `X` and `Y` are topological spaces, `s` is a Lindelöf subset of `X`, `f : X → Y` is a continuous embedding, then the image `f[s]` is a Lindelöf subset of `Y`.
|
Subtype.isLindelof_iff
theorem Subtype.isLindelof_iff :
∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop} {s : Set { x // p x }},
IsLindelof s ↔ IsLindelof (Subtype.val '' s)
The theorem `Subtype.isLindelof_iff` states that for any type `X` with a given topological space structure, a predicate `p` on `X`, and a set `s` of elements of `X` that satisfy `p`, the set `s` is Lindelöf if and only if the image of `s` under the function `Subtype.val` (which extracts the underlying element from the subtype) is also Lindelöf. In simpler terms, a set of elements that satisfy a certain property is Lindelöf if and only if the set of the 'raw' elements, without considering the property, is Lindelöf. In mathematical terms, a set `s` is Lindelöf if for any nontrivial filter `f` with the countable intersection property that contains `s`, there is a cluster point in `s`.
More concisely: A subtype of a topological space is Lindelöf if and only if its underlying set is Lindelöf.
|