# 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 contains s contains a countable subcover. We choose for the equivalent definition where we require that every nontrivial filter on s with the countable intersection property has a clusterpoint. Equivalence is established in isLindelof_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.
def IsLindelof {X : Type u} [] (s : Set X) :

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
• = ∀ ⦃f : ⦄ [inst_1 : f.NeBot] [inst_2 : ], xs,
Instances For
theorem IsLindelof.compl_mem_sets {X : Type u} [] {s : Set X} (hs : ) {f : } (hf : xs, s nhds x f) :
s f

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.

theorem IsLindelof.compl_mem_sets_of_nhdsWithin {X : Type u} [] {s : Set X} (hs : ) {f : } (hf : xs, t, t f) :
s f

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.

theorem IsLindelof.induction_on {X : Type u} [] {s : Set X} (hs : ) {p : Set XProp} (hmono : ∀ ⦃s t : Set X⦄, s tp tp s) (hcountable_union : ∀ (S : Set (Set X)), S.Countable(sS, p s)p (⋃₀ S)) (hnhds : xs, t, p t) :
p s

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.

theorem IsLindelof.inter_right {X : Type u} [] {s : Set X} {t : Set X} (hs : ) (ht : ) :

The intersection of a Lindelöf set and a closed set is a Lindelöf set.

theorem IsLindelof.inter_left {X : Type u} [] {s : Set X} {t : Set X} (ht : ) (hs : ) :

The intersection of a closed set and a Lindelöf set is a Lindelöf set.

theorem IsLindelof.diff {X : Type u} [] {s : Set X} {t : Set X} (hs : ) (ht : ) :

The set difference of a Lindelöf set and an open set is a Lindelöf set.

theorem IsLindelof.of_isClosed_subset {X : Type u} [] {s : Set X} {t : Set X} (hs : ) (ht : ) (h : t s) :

A closed subset of a Lindelöf set is a Lindelöf set.

theorem IsLindelof.image_of_continuousOn {X : Type u} {Y : Type v} [] [] {s : Set X} {f : XY} (hs : ) (hf : ) :

A continuous image of a Lindelöf set is a Lindelöf set.

theorem IsLindelof.image {X : Type u} {Y : Type v} [] [] {s : Set X} {f : XY} (hs : ) (hf : ) :

A continuous image of a Lindelöf set is a Lindelöf set within the codomain.

theorem IsLindelof.adherence_nhdset {X : Type u} [] {s : Set X} {t : Set X} {f : } (hs : ) (hf₂ : ) (ht₁ : ) (ht₂ : xs, x t) :
t f

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.

theorem IsLindelof.elim_countable_subcover {X : Type u} [] {s : Set X} {ι : Type v} (hs : ) (U : ιSet X) (hUo : ∀ (i : ι), IsOpen (U i)) (hsU : s ⋃ (i : ι), U i) :
∃ (r : Set ι), r.Countable s ir, U i

For every open cover of a Lindelöf set, there exists a countable subcover.

theorem IsLindelof.elim_nhds_subcover' {X : Type u} [] {s : Set X} (hs : ) (U : (x : X) → x sSet X) (hU : ∀ (x : X) (hx : x s), U x hx nhds x) :
∃ (t : Set s), t.Countable s xt, U x
theorem IsLindelof.elim_nhds_subcover {X : Type u} [] {s : Set X} (hs : ) (U : XSet X) (hU : xs, U x nhds x) :
∃ (t : Set X), t.Countable (xt, x s) s xt, U x
theorem IsLindelof.indexed_countable_subcover {X : Type u} [] {s : Set X} {ι : Type v} [] (hs : ) (U : ιSet X) (hUo : ∀ (i : ι), IsOpen (U i)) (hsU : s ⋃ (i : ι), U i) :
∃ (f : ι), s ⋃ (n : ), U (f n)

For every nonempty open cover of a Lindelöf set, there exists a subcover indexed by ℕ.

theorem IsLindelof.disjoint_nhdsSet_left {X : Type u} [] {s : Set X} {l : } (hs : ) :
Disjoint () l xs, Disjoint (nhds x) l

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.

theorem IsLindelof.disjoint_nhdsSet_right {X : Type u} [] {s : Set X} {l : } (hs : ) :
Disjoint l () xs, Disjoint l (nhds x)

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.

theorem IsLindelof.elim_countable_subfamily_closed {X : Type u} [] {s : Set X} {ι : Type v} (hs : ) (t : ιSet X) (htc : ∀ (i : ι), IsClosed (t i)) (hst : s ⋂ (i : ι), t i = ) :
∃ (u : Set ι), u.Countable s iu, t i =

For every family of closed sets whose intersection avoids a Lindelö set, there exists a countable subfamily whose intersection avoids this Lindelöf set.

theorem IsLindelof.inter_iInter_nonempty {X : Type u} [] {s : Set X} {ι : Type v} (hs : ) (t : ιSet X) (htc : ∀ (i : ι), IsClosed (t i)) (hst : ∀ (u : Set ι), u.Countable (s iu, t i).Nonempty) :
(s ⋂ (i : ι), t i).Nonempty

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.

theorem IsLindelof.elim_countable_subcover_image {X : Type u} {ι : Type u_1} [] {s : Set X} {b : Set ι} {c : ιSet X} (hs : ) (hc₁ : ib, IsOpen (c i)) (hc₂ : s ib, c i) :
b'b, b'.Countable s ib', c i

For every open cover of a Lindelöf set, there exists a countable subcover.

theorem isLindelof_of_countable_subcover {X : Type u} [] {s : Set X} (h : ∀ {ι : Type u} (U : ιSet X), (∀ (i : ι), IsOpen (U i))s ⋃ (i : ι), U i∃ (t : Set ι), t.Countable s it, U i) :

A set s is Lindelöf if for every open cover of s, there exists a countable subcover.

theorem isLindelof_of_countable_subfamily_closed {X : Type u} [] {s : Set X} (h : ∀ {ι : Type u} (t : ιSet X), (∀ (i : ι), IsClosed (t i))s ⋂ (i : ι), t i = ∃ (u : Set ι), u.Countable s iu, t i = ) :

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.

theorem isLindelof_iff_countable_subcover {X : Type u} [] {s : Set X} :
∀ {ι : Type u} (U : ιSet X), (∀ (i : ι), IsOpen (U i))s ⋃ (i : ι), U i∃ (t : Set ι), t.Countable s it, U i

A set s is Lindelöf if and only if for every open cover of s, there exists a countable subcover.

theorem isLindelof_iff_countable_subfamily_closed {X : Type u} [] {s : Set X} :
∀ {ι : Type u} (t : ιSet X), (∀ (i : ι), IsClosed (t i))s ⋂ (i : ι), t i = ∃ (u : Set ι), u.Countable s iu, t i =

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.

@[simp]
theorem isLindelof_empty {X : Type u} [] :

The empty set is a Lindelof set.

@[simp]
theorem isLindelof_singleton {X : Type u} [] {x : X} :

A singleton set is a Lindelof set.

theorem Set.Subsingleton.isLindelof {X : Type u} [] {s : Set X} (hs : s.Subsingleton) :
theorem Set.Countable.isLindelof_biUnion {X : Type u} {ι : Type u_1} [] {s : Set ι} {f : ιSet X} (hs : s.Countable) (hf : is, IsLindelof (f i)) :
IsLindelof (is, f i)
theorem Set.Finite.isLindelof_biUnion {X : Type u} {ι : Type u_1} [] {s : Set ι} {f : ιSet X} (hs : s.Finite) (hf : is, IsLindelof (f i)) :
IsLindelof (is, f i)
theorem Finset.isLindelof_biUnion {X : Type u} {ι : Type u_1} [] (s : ) {f : ιSet X} (hf : is, IsLindelof (f i)) :
IsLindelof (is, f i)
theorem isLindelof_accumulate {X : Type u} [] {K : Set X} (hK : ∀ (n : ), IsLindelof (K n)) (n : ) :
theorem Set.Countable.isLindelof_sUnion {X : Type u} [] {S : Set (Set X)} (hf : S.Countable) (hc : sS, ) :
theorem Set.Finite.isLindelof_sUnion {X : Type u} [] {S : Set (Set X)} (hf : S.Finite) (hc : sS, ) :
theorem isLindelof_iUnion {X : Type u} [] {ι : Sort u_2} {f : ιSet X} [] (h : ∀ (i : ι), IsLindelof (f i)) :
IsLindelof (⋃ (i : ι), f i)
theorem Set.Countable.isLindelof {X : Type u} [] {s : Set X} (hs : s.Countable) :
theorem Set.Finite.isLindelof {X : Type u} [] {s : Set X} (hs : s.Finite) :
theorem IsLindelof.countable_of_discrete {X : Type u} [] {s : Set X} [] (hs : ) :
s.Countable
theorem isLindelof_iff_countable {X : Type u} [] {s : Set X} [] :
s.Countable
theorem IsLindelof.union {X : Type u} [] {s : Set X} {t : Set X} (hs : ) (ht : ) :
theorem IsLindelof.insert {X : Type u} [] {s : Set X} (hs : ) (a : X) :
theorem isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis {X : Type u} {ι : Type u_1} [] (b : ιSet X) (hb : ) (hb' : ∀ (i : ι), IsLindelof (b i)) (U : Set X) :
∃ (s : Set ι), s.Countable U = is, b i

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

def Filter.coLindelof (X : Type u_2) [] :

Filter.coLindelof is the filter generated by complements to Lindelöf sets.

Equations
• = ⨅ (s : Set X), ⨅ (_ : ),
Instances For
theorem hasBasis_coLindelof {X : Type u} [] :
.HasBasis IsLindelof compl
theorem mem_coLindelof {X : Type u} [] {s : Set X} :
∃ (t : Set X), t s
theorem mem_coLindelof' {X : Type u} [] {s : Set X} :
∃ (t : Set X), s t
theorem IsLindelof.compl_mem_coLindelof {X : Type u} [] {s : Set X} (hs : ) :
theorem coLindelof_le_cofinite {X : Type u} [] :
Filter.cofinite
theorem Tendsto.isLindelof_insert_range_of_coLindelof {X : Type u} {Y : Type v} [] [] {f : XY} {y : Y} (hf : Filter.Tendsto f (nhds y)) (hfc : ) :
def Filter.coclosedLindelof (X : Type u_2) [] :

Filter.coclosedLindelof is the filter generated by complements to closed Lindelof sets.

Equations
• = ⨅ (s : Set X), ⨅ (_ : ), ⨅ (_ : ),
Instances For
theorem hasBasis_coclosedLindelof {X : Type u} [] :
.HasBasis (fun (s : Set X) => ) compl
theorem mem_coclosedLindelof {X : Type u} [] {s : Set X} :
∃ (t : Set X), t s
theorem mem_coclosed_Lindelof' {X : Type u} [] {s : Set X} :
∃ (t : Set X), s t
theorem IsLindeof.compl_mem_coclosedLindelof_of_isClosed {X : Type u} [] {s : Set X} (hs : ) (hs' : ) :
class LindelofSpace (X : Type u_2) [] :

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
theorem LindelofSpace.isLindelof_univ {X : Type u_2} [] [self : ] :
IsLindelof Set.univ

In a Lindelöf space, Set.univ is a Lindelöf set.

@[instance 10]
instance Subsingleton.lindelofSpace {X : Type u} [] [] :
Equations
• =
theorem isLindelof_univ_iff {X : Type u} [] :
IsLindelof Set.univ
theorem isLindelof_univ {X : Type u} [] [h : ] :
IsLindelof Set.univ
theorem cluster_point_of_Lindelof {X : Type u} [] [] (f : ) [f.NeBot] :
∃ (x : X),
theorem LindelofSpace.elim_nhds_subcover {X : Type u} [] [] (U : XSet X) (hU : ∀ (x : X), U x nhds x) :
∃ (t : Set X), t.Countable xt, U x = Set.univ
theorem lindelofSpace_of_countable_subfamily_closed {X : Type u} [] (h : ∀ {ι : Type u} (t : ιSet X), (∀ (i : ι), IsClosed (t i))⋂ (i : ι), t i = ∃ (u : Set ι), u.Countable iu, t i = ) :
theorem IsClosed.isLindelof {X : Type u} [] {s : Set X} [] (h : ) :
theorem IsCompact.isLindelof {X : Type u} [] {s : Set X} (hs : ) :

A compact set s is Lindelöf.

theorem IsSigmaCompact.isLindelof {X : Type u} [] {s : Set X} (hs : ) :

A σ-compact set s is Lindelöf

@[instance 100]
instance instLindelofSpaceOfCompactSpace {X : Type u} [] [] :

A compact space X is Lindelöf.

Equations
• =
@[instance 100]

A sigma-compact space X is Lindelöf.

Equations
• =
class NonLindelofSpace (X : Type u_2) [] :

X is a non-Lindelöf topological space if it is not a Lindelöf space.

• nonLindelof_univ : ¬IsLindelof Set.univ

In a non-Lindelöf space, Set.univ is not a Lindelöf set.

Instances
theorem NonLindelofSpace.nonLindelof_univ {X : Type u_2} [] [self : ] :
¬IsLindelof Set.univ

In a non-Lindelöf space, Set.univ is not a Lindelöf set.

theorem nonLindelof_univ (X : Type u_2) [] [] :
¬IsLindelof Set.univ
theorem IsLindelof.ne_univ {X : Type u} [] {s : Set X} [] (hs : ) :
s Set.univ
instance instNeBotCoLindelofOfNonLindelofSpace {X : Type u} [] [] :
.NeBot
Equations
• =
@[simp]
theorem Filter.coLindelof_eq_bot {X : Type u} [] [] :
instance instNeBotCoclosedLindelofOfNonLindelofSpace {X : Type u} [] [] :
.NeBot
Equations
• =
theorem nonLindelofSpace_of_neBot {X : Type u} [] :
.NeBot
theorem Filter.coLindelof_neBot_iff {X : Type u} [] :
.NeBot
theorem not_LindelofSpace_iff {X : Type u} [] :
@[instance 100]
instance instLindelofSpaceOfCompactSpace_1 {X : Type u} [] [] :

A compact space X is Lindelöf.

Equations
• =
theorem countable_cover_nhds_interior {X : Type u} [] [] {U : XSet X} (hU : ∀ (x : X), U x nhds x) :
∃ (t : Set X), t.Countable xt, interior (U x) = Set.univ
theorem countable_cover_nhds {X : Type u} [] [] {U : XSet X} (hU : ∀ (x : X), U x nhds x) :
∃ (t : Set X), t.Countable xt, U x = Set.univ
theorem Filter.comap_coLindelof_le {X : Type u} {Y : Type v} [] [] {f : XY} (hf : ) :

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.

theorem isLindelof_range {X : Type u} {Y : Type v} [] [] [] {f : XY} (hf : ) :
theorem isLindelof_diagonal {X : Type u} [] [] :
theorem Inducing.isLindelof_iff {X : Type u} {Y : Type v} [] [] {s : Set X} {f : XY} (hf : ) :

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.

theorem Embedding.isLindelof_iff {X : Type u} {Y : Type v} [] [] {s : Set X} {f : XY} (hf : ) :

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.

theorem Inducing.isLindelof_preimage {X : Type u} {Y : Type v} [] [] {f : XY} (hf : ) (hf' : ) {K : Set Y} (hK : ) :

The preimage of a Lindelöf set under an inducing map is a Lindelöf set.

theorem ClosedEmbedding.isLindelof_preimage {X : Type u} {Y : Type v} [] [] {f : XY} (hf : ) {K : Set Y} (hK : ) :

The preimage of a Lindelöf set under a closed embedding is a Lindelöf set.

theorem ClosedEmbedding.tendsto_coLindelof {X : Type u} {Y : Type v} [] [] {f : XY} (hf : ) :

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 ClosedEmbedding.isLindelof_preimage.

theorem Subtype.isLindelof_iff {X : Type u} [] {p : XProp} {s : Set { x : X // p x }} :
IsLindelof (Subtype.val '' s)

Sets of subtype are Lindelöf iff the image under a coercion is.

theorem isLindelof_iff_isLindelof_univ {X : Type u} [] {s : Set X} :
IsLindelof Set.univ
theorem isLindelof_iff_LindelofSpace {X : Type u} [] {s : Set X} :
theorem IsLindelof.of_coe {X : Type u} [] {s : Set X} [] :
theorem IsLindelof.countable {X : Type u} [] {s : Set X} (hs : ) (hs' : ) :
s.Countable
theorem ClosedEmbedding.nonLindelofSpace {X : Type u} {Y : Type v} [] [] [] {f : XY} (hf : ) :
theorem ClosedEmbedding.LindelofSpace {X : Type u} {Y : Type v} [] [] [h : ] {f : XY} (hf : ) :
@[instance 100]
instance Countable.LindelofSpace {X : Type u} [] [] :

Countable topological spaces are Lindelof.

Equations
• =
instance instLindelofSpaceSum {X : Type u} {Y : Type v} [] [] [] [] :

The disjoint union of two Lindelöf spaces is Lindelöf.

Equations
• =
instance instLindelofSpaceSigmaOfCountable {ι : Type u_1} {X : ιType u_2} [] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), LindelofSpace (X i)] :
LindelofSpace ((i : ι) × X i)
Equations
• =
instance Quot.LindelofSpace {X : Type u} [] {r : XXProp} [] :
Equations
• =
instance Quotient.LindelofSpace {X : Type u} [] {s : } [] :
Equations
• =
theorem LindelofSpace.of_continuous_surjective {X : Type u} {Y : Type v} [] [] {f : XY} [] (hf : ) (hsur : ) :

A continuous image of a Lindelöf set is a Lindelöf set within the codomain.

def IsHereditarilyLindelof {X : Type u} [] (s : Set X) :

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.

Equations
• = ts,
Instances For
class HereditarilyLindelofSpace (X : Type u_2) [] :

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.

Instances

In a Hereditarily Lindelöf space, Set.univ is a Hereditarily Lindelöf set.

theorem IsHereditarilyLindelof.isLindelof_subset {X : Type u} [] {s : Set X} {t : Set X} (hs : ) (ht : t s) :
theorem IsHereditarilyLindelof.isLindelof {X : Type u} [] {s : Set X} (hs : ) :
@[instance 100]
Equations
• =
theorem HereditarilyLindelof_LindelofSets {X : Type u} [] (s : Set X) :
@[instance 100]
Equations
• =
theorem eq_open_union_countable {X : Type u} [] {ι : Type u} (U : ιSet X) (h : ∀ (i : ι), IsOpen (U i)) :
∃ (t : Set ι), t.Countable it, U i = ⋃ (i : ι), U i
instance HereditarilyLindelof.lindelofSpace_subtype {X : Type u} [] (p : XProp) :
LindelofSpace { x : X // p x }
Equations
• =