Lindelöf sets and Lindelöf spaces #
Main definitions #
We define the following properties for sets in a topological space:
IsLindelof s
: Two definitions are possible here. The more standard definition is that every open cover that containss
contains a countable subcover. We choose for the equivalent definition where we require that every nontrivial filter ons
with the countable intersection property has a clusterpoint. Equivalence is established inisLindelof_iff_countable_subcover
.LindelofSpace X
:X
is Lindelöf if it is Lindelöf as a set.NonLindelofSpace
: a space that is not a Lindëlof space, e.g. the Long Line.
Main results #
isLindelof_iff_countable_subcover
: A set is Lindelöf iff every open cover has a countable subcover.
Implementation details #
- This API is mainly based on the API for IsCompact and follows notation and style as much as possible.
A set s
is Lindelöf if every nontrivial filter f
with the countable intersection
property that contains s
, has a clusterpoint in s
. The filter-free definition is given by
isLindelof_iff_countable_subcover
.
Equations
- IsLindelof s = ∀ ⦃f : Filter X⦄ [inst : f.NeBot] [inst : CountableInterFilter f], f ≤ Filter.principal s → ∃ x ∈ s, ClusterPt x f
Instances For
The complement to a Lindelöf set belongs to a filter f
with the countable intersection
property if it belongs to each filter 𝓝 x ⊓ f
, x ∈ s
.
The complement to a Lindelöf set belongs to a filter f
with the countable intersection
property if each x ∈ s
has a neighborhood t
within s
such that tᶜ
belongs to f
.
If p : Set X → Prop
is stable under restriction and union, and each point x
of a Lindelöf set s
has a neighborhood t
within s
such that p t
, then p s
holds.
The intersection of a Lindelöf set and a closed set is a Lindelöf set.
The intersection of a closed set and a Lindelöf set is a Lindelöf set.
The set difference of a Lindelöf set and an open set is a Lindelöf set.
A closed subset of a Lindelöf set is a Lindelöf set.
A continuous image of a Lindelöf set is a Lindelöf set.
A continuous image of a Lindelöf set is a Lindelöf set within the codomain.
A filter with the countable intersection property that is finer than the principal filter on
a Lindelöf set s
contains any open set that contains all clusterpoints of s
.
For every open cover of a Lindelöf set, there exists a countable subcover.
For every nonempty open cover of a Lindelöf set, there exists a subcover indexed by ℕ.
The neighborhood filter of a Lindelöf set is disjoint with a filter l
with the countable
intersection property if and only if the neighborhood filter of each point of this set
is disjoint with l
.
A filter l
with the countable intersection property is disjoint with the neighborhood
filter of a Lindelöf set if and only if it is disjoint with the neighborhood filter of each point
of this set.
For every family of closed sets whose intersection avoids a Lindelö set, there exists a countable subfamily whose intersection avoids this Lindelöf set.
To show that a Lindelöf set intersects the intersection of a family of closed sets, it is sufficient to show that it intersects every countable subfamily.
For every open cover of a Lindelöf set, there exists a countable subcover.
A set s
is Lindelöf if for every open cover of s
, there exists a countable subcover.
A set s
is Lindelöf if for every family of closed sets whose intersection avoids s
,
there exists a countable subfamily whose intersection avoids s
.
A set s
is Lindelöf if and only if
for every open cover of s
, there exists a countable subcover.
A set s
is Lindelöf if and only if
for every family of closed sets whose intersection avoids s
,
there exists a countable subfamily whose intersection avoids s
.
The empty set is a Lindelof set.
A singleton set is a Lindelof set.
If X
has a basis consisting of compact opens, then an open set in X
is compact open iff
it is a finite union of some elements in the basis
Filter.coclosedLindelof
is the filter generated by complements to closed Lindelof sets.
Equations
Instances For
X is a Lindelöf space iff every open cover has a countable subcover.
- isLindelof_univ : IsLindelof Set.univ
In a Lindelöf space,
Set.univ
is a Lindelöf set.
Instances
A compact set s
is Lindelöf.
A σ-compact set s
is Lindelöf
A compact space X
is Lindelöf.
A sigma-compact space X
is Lindelöf.
X
is a non-Lindelöf topological space if it is not a Lindelöf space.
In a non-Lindelöf space,
Set.univ
is not a Lindelöf set.
Instances
A compact space X
is Lindelöf.
The comap of the coLindelöf filter on Y
by a continuous function f : X → Y
is less than or
equal to the coLindelöf filter on X
.
This is a reformulation of the fact that images of Lindelöf sets are Lindelöf.
If f : X → Y
is an inducing map, the image f '' s
of a set s
is Lindelöf
if and only if s
is compact.
Alias of Topology.IsInducing.isLindelof_iff
.
If f : X → Y
is an inducing map, the image f '' s
of a set s
is Lindelöf
if and only if s
is compact.
If f : X → Y
is an embedding, the image f '' s
of a set s
is Lindelöf
if and only if s
is Lindelöf.
Alias of Topology.IsEmbedding.isLindelof_iff
.
If f : X → Y
is an embedding, the image f '' s
of a set s
is Lindelöf
if and only if s
is Lindelöf.
The preimage of a Lindelöf set under an inducing map is a Lindelöf set.
Alias of Topology.IsInducing.isLindelof_preimage
.
The preimage of a Lindelöf set under an inducing map is a Lindelöf set.
The preimage of a Lindelöf set under a closed embedding is a Lindelöf set.
Alias of Topology.IsClosedEmbedding.isLindelof_preimage
.
The preimage of a Lindelöf set under a closed embedding is a Lindelöf set.
A closed embedding is proper, ie, inverse images of Lindelöf sets are contained in Lindelöf.
Moreover, the preimage of a Lindelöf set is Lindelöf, see
Topology.IsClosedEmbedding.isLindelof_preimage
.
Alias of Topology.IsClosedEmbedding.tendsto_coLindelof
.
A closed embedding is proper, ie, inverse images of Lindelöf sets are contained in Lindelöf.
Moreover, the preimage of a Lindelöf set is Lindelöf, see
Topology.IsClosedEmbedding.isLindelof_preimage
.
Sets of subtype are Lindelöf iff the image under a coercion is.
Alias of Topology.IsClosedEmbedding.LindelofSpace
.
Countable topological spaces are Lindelof.
The disjoint union of two Lindelöf spaces is Lindelöf.
A continuous image of a Lindelöf set is a Lindelöf set within the codomain.
A set s
is Hereditarily Lindelöf if every subset is a Lindelof set. We require this only
for open sets in the definition, and then conclude that this holds for all sets by ADD.
Instances For
Type class for Hereditarily Lindelöf spaces.
- isHereditarilyLindelof_univ : IsHereditarilyLindelof Set.univ
In a Hereditarily Lindelöf space,
Set.univ
is a Hereditarily Lindelöf set.