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} [TopologicalSpace X] (s : Set X) : Prop

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_1 : Filter.NeBot f] [inst_2 : CountableInterFilter f], f ≤ Filter.principal s → ∃ x ∈ s, ClusterPt x f

theorem IsLindelof.compl_mem_sets {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsLindelof s) {f : Filter X} [CountableInterFilter f] (hf : ∀ x ∈ s, 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} [TopologicalSpace X] {s : Set X} (hs : IsLindelof s) {f : Filter X} [CountableInterFilter f] (hf : ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, 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} [TopologicalSpace X] {s : Set X} (hs : IsLindelof s) {p : Set X → Prop} (hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s) (hcountable_union : ∀ (S : Set (Set X)), Set.Countable S → (∀ s ∈ S, p s) → p (⋃₀ S)) (hnhds : ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, 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} [TopologicalSpace X] {s : Set X} {t : Set X} (hs : IsLindelof s) (ht : IsClosed t) : IsLindelof (s ∩ t)

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

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

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

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

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} [TopologicalSpace X] {s : Set X} {t : Set X} (hs : IsLindelof s) (ht : IsClosed t) (h : t ⊆ s) : IsLindelof t

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

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

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

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

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

theorem IsLindelof.adherence_nhdset {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} {f : Filter X} [CountableInterFilter f] (hs : IsLindelof s) (hf₂ : f ≤ Filter.principal s) (ht₁ : IsOpen t) (ht₂ : ∀ x ∈ s, ClusterPt x f → 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} [TopologicalSpace X] {s : Set X} {ι : Type v} (hs : IsLindelof s) (U : ι → Set X) (hUo : ∀ (i : ι), IsOpen (U i)) (hsU : s ⊆ ⋃ (i : ι), U i) : ∃ (r : Set ι), Set.Countable r ∧ s ⊆ ⋃ i ∈ r, U i

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

theorem IsLindelof.elim_nhds_subcover' {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsLindelof s) (U : (x : X) → x ∈ s → Set X) (hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ nhds x) : ∃ (t : Set ↑s), Set.Countable t ∧ s ⊆ ⋃ x ∈ t, U ↑x (_ : ↑x ∈ s)

theorem IsLindelof.elim_nhds_subcover {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsLindelof s) (U : X → Set X) (hU : ∀ x ∈ s, U x ∈ nhds x) : ∃ (t : Set X), Set.Countable t ∧ (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x

theorem IsLindelof.disjoint_nhdsSet_left {X : Type u} [TopologicalSpace X] {s : Set X} {l : Filter X} [CountableInterFilter l] (hs : IsLindelof s) : Disjoint (nhdsSet s) l ↔ ∀ x ∈ s, 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} [TopologicalSpace X] {s : Set X} {l : Filter X} [CountableInterFilter l] (hs : IsLindelof s) : Disjoint l (nhdsSet s) ↔ ∀ x ∈ s, 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} [TopologicalSpace X] {s : Set X} {ι : Type v} (hs : IsLindelof s) (t : ι → Set X) (htc : ∀ (i : ι), IsClosed (t i)) (hst : s ∩ ⋂ (i : ι), t i = ∅) : ∃ (u : Set ι), Set.Countable u ∧ s ∩ ⋂ i ∈ u, 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} [TopologicalSpace X] {s : Set X} {ι : Type v} (hs : IsLindelof s) (t : ι → Set X) (htc : ∀ (i : ι), IsClosed (t i)) (hst : ∀ (u : Set ι), Set.Countable u ∧ Set.Nonempty (s ∩ ⋂ i ∈ u, t i)) : Set.Nonempty (s ∩ ⋂ (i : ι), t i)

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} [TopologicalSpace X] {s : Set X} {b : Set ι} {c : ι → Set X} (hs : IsLindelof s) (hc₁ : ∀ i ∈ b, IsOpen (c i)) (hc₂ : s ⊆ ⋃ i ∈ b, c i) : ∃ b' ⊆ b, Set.Countable b' ∧ s ⊆ ⋃ i ∈ b', c i

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

theorem isLindelof_of_countable_subcover {X : Type u} [TopologicalSpace X] {s : Set X} (h : ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ (i : ι), U i → ∃ (t : Set ι), Set.Countable t ∧ s ⊆ ⋃ i ∈ t, U i) : IsLindelof s

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} [TopologicalSpace X] {s : Set X} (h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ (i : ι), t i = ∅ → ∃ (u : Set ι), Set.Countable u ∧ s ∩ ⋂ i ∈ u, t i = ∅) : IsLindelof s

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} [TopologicalSpace X] {s : Set X} : IsLindelof s ↔ ∀ {ι : Type u} (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ (i : ι), U i → ∃ (t : Set ι), Set.Countable t ∧ s ⊆ ⋃ i ∈ t, 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} [TopologicalSpace X] {s : Set X} : IsLindelof s ↔ ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ (i : ι), t i = ∅ → ∃ (u : Set ι), Set.Countable u ∧ s ∩ ⋂ i ∈ u, 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} [TopologicalSpace X] : IsLindelof ∅

The empty set is a Lindelof set.

@[simp]

theorem isLindelof_singleton {X : Type u} [TopologicalSpace X] {x : X} : IsLindelof {x}

A singleton set is a Lindelof set.

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

theorem Set.Countable.isLindelof_biUnion {X : Type u} {ι : Type u_1} [TopologicalSpace X] {s : Set ι} {f : ι → Set X} (hs : Set.Countable s) (hf : ∀ i ∈ s, IsLindelof (f i)) : IsLindelof (⋃ i ∈ s, f i)

theorem Set.Finite.isLindelof_biUnion {X : Type u} {ι : Type u_1} [TopologicalSpace X] {s : Set ι} {f : ι → Set X} (hs : Set.Finite s) (hf : ∀ i ∈ s, IsLindelof (f i)) : IsLindelof (⋃ i ∈ s, f i)

theorem Finset.isLindelof_biUnion {X : Type u} {ι : Type u_1} [TopologicalSpace X] (s : Finset ι) {f : ι → Set X} (hf : ∀ i ∈ s, IsLindelof (f i)) : IsLindelof (⋃ i ∈ s, f i)

theorem isLindelof_accumulate {X : Type u} [TopologicalSpace X] {K : ℕ → Set X} (hK : ∀ (n : ℕ), IsLindelof (K n)) (n : ℕ) : IsLindelof (Set.Accumulate K n)

theorem Set.Countable.isLindelof_sUnion {X : Type u} [TopologicalSpace X] {S : Set (Set X)} (hf : Set.Countable S) (hc : ∀ s ∈ S, IsLindelof s) : IsLindelof (⋃₀ S)

theorem Set.Finite.isLindelof_sUnion {X : Type u} [TopologicalSpace X] {S : Set (Set X)} (hf : Set.Finite S) (hc : ∀ s ∈ S, IsLindelof s) : IsLindelof (⋃₀ S)

theorem isLindelof_iUnion {X : Type u} [TopologicalSpace X] {ι : Sort u_2} {f : ι → Set X} [Countable ι] (h : ∀ (i : ι), IsLindelof (f i)) : IsLindelof (⋃ (i : ι), f i)

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

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

theorem IsLindelof.countable_of_discrete {X : Type u} [TopologicalSpace X] {s : Set X} [DiscreteTopology X] (hs : IsLindelof s) : Set.Countable s

theorem isLindelof_iff_countable {X : Type u} [TopologicalSpace X] {s : Set X} [DiscreteTopology X] : IsLindelof s ↔ Set.Countable s

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

theorem IsLindelof.insert {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsLindelof s) (a : X) : IsLindelof (insert a s)

theorem isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis {X : Type u} {ι : Type u_1} [TopologicalSpace X] (b : ι → Set X) (hb : TopologicalSpace.IsTopologicalBasis (Set.range b)) (hb' : ∀ (i : ι), IsLindelof (b i)) (U : Set X) : IsLindelof U ∧ IsOpen U ↔ ∃ (s : Set ι), Set.Countable s ∧ U = ⋃ i ∈ s, 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) [TopologicalSpace X] : Filter X

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

Equations

• Filter.coLindelof X = ⨅ (s : Set X), ⨅ (_ : IsLindelof s), Filter.principal sᶜ

theorem hasBasis_coLindelof {X : Type u} [TopologicalSpace X] : Filter.HasBasis (Filter.coLindelof X) IsLindelof compl

theorem mem_coLindelof {X : Type u} [TopologicalSpace X] {s : Set X} : s ∈ Filter.coLindelof X ↔ ∃ (t : Set X), IsLindelof t ∧ tᶜ ⊆ s

theorem mem_coLindelof' {X : Type u} [TopologicalSpace X] {s : Set X} : s ∈ Filter.coLindelof X ↔ ∃ (t : Set X), IsLindelof t ∧ sᶜ ⊆ t

theorem IsLindelof.compl_mem_coLindelof {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsLindelof s) : sᶜ ∈ Filter.coLindelof X

theorem coLindelof_le_cofinite {X : Type u} [TopologicalSpace X] : Filter.coLindelof X ≤ Filter.cofinite

theorem Tendsto.isLindelof_insert_range_of_coLindelof {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {y : Y} (hf : Filter.Tendsto f (Filter.coLindelof X) (nhds y)) (hfc : Continuous f) : IsLindelof (insert y (Set.range f))

def Filter.coclosedLindelof (X : Type u_2) [TopologicalSpace X] : Filter X

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

Equations

• Filter.coclosedLindelof X = ⨅ (s : Set X), ⨅ (_ : IsClosed s), ⨅ (_ : IsLindelof s), Filter.principal sᶜ

theorem hasBasis_coclosedLindelof {X : Type u} [TopologicalSpace X] : Filter.HasBasis (Filter.coclosedLindelof X) (fun (s : Set X) => IsClosed s ∧ IsLindelof s) compl

theorem mem_coclosedLindelof {X : Type u} [TopologicalSpace X] {s : Set X} : s ∈ Filter.coclosedLindelof X ↔ ∃ (t : Set X), IsClosed t ∧ IsLindelof t ∧ tᶜ ⊆ s

theorem mem_coclosed_Lindelof' {X : Type u} [TopologicalSpace X] {s : Set X} : s ∈ Filter.coclosedLindelof X ↔ ∃ (t : Set X), IsClosed t ∧ IsLindelof t ∧ sᶜ ⊆ t

theorem coLindelof_le_coclosedLindelof {X : Type u} [TopologicalSpace X] : Filter.coLindelof X ≤ Filter.coclosedLindelof X

theorem IsLindeof.compl_mem_coclosedLindelof_of_isClosed {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsLindelof s) (hs' : IsClosed s) : sᶜ ∈ Filter.coclosedLindelof X

class LindelofSpace (X : Type u_2) [TopologicalSpace X] : Prop

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.

instance Subsingleton.lindelofSpace {X : Type u} [TopologicalSpace X] [Subsingleton X] : LindelofSpace X

Equations

• (_ : LindelofSpace X) = (_ : LindelofSpace X)

theorem isLindelof_univ_iff {X : Type u} [TopologicalSpace X] : IsLindelof Set.univ ↔ LindelofSpace X

theorem isLindelof_univ {X : Type u} [TopologicalSpace X] [h : LindelofSpace X] : IsLindelof Set.univ

theorem cluster_point_of_Lindelof {X : Type u} [TopologicalSpace X] [LindelofSpace X] (f : Filter X) [Filter.NeBot f] [CountableInterFilter f] : ∃ (x : X), ClusterPt x f

theorem LindelofSpace.elim_nhds_subcover {X : Type u} [TopologicalSpace X] [LindelofSpace X] (U : X → Set X) (hU : ∀ (x : X), U x ∈ nhds x) : ∃ (t : Set X), Set.Countable t ∧ ⋃ x ∈ t, U x = Set.univ

theorem lindelofSpace_of_countable_subfamily_closed {X : Type u} [TopologicalSpace X] (h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → ⋂ (i : ι), t i = ∅ → ∃ (u : Set ι), Set.Countable u ∧ ⋂ i ∈ u, t i = ∅) : LindelofSpace X

theorem IsClosed.isLindelof {X : Type u} [TopologicalSpace X] {s : Set X} [LindelofSpace X] (h : IsClosed s) : IsLindelof s

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

A compact set s is Lindelöf.

instance instLindelofSpace {X : Type u} [TopologicalSpace X] [CompactSpace X] : LindelofSpace X

A compact space X is Lindelöf.

Equations

• (_ : LindelofSpace X) = (_ : LindelofSpace X)

class NonLindelofSpace (X : Type u_2) [TopologicalSpace X] : Prop

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.

theorem nonLindelof_univ (X : Type u_2) [TopologicalSpace X] [NonLindelofSpace X] : ¬IsLindelof Set.univ

theorem IsLindelof.ne_univ {X : Type u} [TopologicalSpace X] {s : Set X} [NonLindelofSpace X] (hs : IsLindelof s) : s ≠ Set.univ

instance instNeBotCoLindelof {X : Type u} [TopologicalSpace X] [NonLindelofSpace X] : Filter.NeBot (Filter.coLindelof X)

Equations

• (_ : Filter.NeBot (Filter.coLindelof X)) = (_ : Filter.NeBot (Filter.coLindelof X))

@[simp]

theorem Filter.coLindelof_eq_bot {X : Type u} [TopologicalSpace X] [LindelofSpace X] : Filter.coLindelof X = ⊥

instance instNeBotCoclosedLindelof {X : Type u} [TopologicalSpace X] [NonLindelofSpace X] : Filter.NeBot (Filter.coclosedLindelof X)

Equations

• (_ : Filter.NeBot (Filter.coclosedLindelof X)) = (_ : Filter.NeBot (Filter.coclosedLindelof X))

theorem nonLindelofSpace_of_neBot {X : Type u} [TopologicalSpace X] : Filter.NeBot (Filter.coLindelof X) → NonLindelofSpace X

theorem Filter.coLindelof_neBot_iff {X : Type u} [TopologicalSpace X] : Filter.NeBot (Filter.coLindelof X) ↔ NonLindelofSpace X

theorem not_LindelofSpace_iff {X : Type u} [TopologicalSpace X] : ¬LindelofSpace X ↔ NonLindelofSpace X

instance instLindelofSpace_1 {X : Type u} [TopologicalSpace X] [CompactSpace X] : LindelofSpace X

A compact space X is Lindelöf.

Equations

• (_ : LindelofSpace X) = (_ : LindelofSpace X)

theorem countable_of_Lindelof_of_discrete {X : Type u} [TopologicalSpace X] [LindelofSpace X] [DiscreteTopology X] : Countable X

theorem countable_cover_nhds_interior {X : Type u} [TopologicalSpace X] [LindelofSpace X] {U : X → Set X} (hU : ∀ (x : X), U x ∈ nhds x) : ∃ (t : Set X), Set.Countable t ∧ ⋃ x ∈ t, interior (U x) = Set.univ

theorem countable_cover_nhds {X : Type u} [TopologicalSpace X] [LindelofSpace X] {U : X → Set X} (hU : ∀ (x : X), U x ∈ nhds x) : ∃ (t : Set X), Set.Countable t ∧ ⋃ x ∈ t, U x = Set.univ

theorem Filter.comap_coLindelof_le {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) : Filter.comap f (Filter.coLindelof Y) ≤ Filter.coLindelof X

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} [TopologicalSpace X] [TopologicalSpace Y] [LindelofSpace X] {f : X → Y} (hf : Continuous f) : IsLindelof (Set.range f)

theorem isLindelof_diagonal {X : Type u} [TopologicalSpace X] [LindelofSpace X] : IsLindelof (Set.diagonal X)

theorem Inducing.isLindelof_iff {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf : Inducing f) : IsLindelof s ↔ IsLindelof (f '' s)

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} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf : Embedding f) : IsLindelof s ↔ IsLindelof (f '' s)

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} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Inducing f) (hf' : IsClosed (Set.range f)) {K : Set Y} (hK : IsLindelof K) : IsLindelof (f ⁻¹' K)

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} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : ClosedEmbedding f) {K : Set Y} (hK : IsLindelof K) : IsLindelof (f ⁻¹' K)

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} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : ClosedEmbedding f) : Filter.Tendsto f (Filter.coLindelof X) (Filter.coLindelof Y)

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} [TopologicalSpace X] {p : X → Prop} {s : Set { x : X // p x }} : IsLindelof s ↔ 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} [TopologicalSpace X] {s : Set X} : IsLindelof s ↔ IsLindelof Set.univ

theorem isLindelof_iff_LindelofSpace {X : Type u} [TopologicalSpace X] {s : Set X} : IsLindelof s ↔ LindelofSpace ↑s

theorem IsLindelof.of_coe {X : Type u} [TopologicalSpace X] {s : Set X} [LindelofSpace ↑s] : IsLindelof s

theorem IsLindelof.countable {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsLindelof s) (hs' : DiscreteTopology ↑s) : Set.Countable s

theorem ClosedEmbedding.nonLindelofSpace {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [NonLindelofSpace X] {f : X → Y} (hf : ClosedEmbedding f) : NonLindelofSpace Y

theorem ClosedEmbedding.LindelofSpace {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [h : LindelofSpace Y] {f : X → Y} (hf : ClosedEmbedding f) : LindelofSpace X

instance Countable.LindelofSpace {X : Type u} [TopologicalSpace X] [Countable X] : LindelofSpace X

Countable topological spaces are Lindelof.

Equations

• (_ : LindelofSpace X) = (_ : LindelofSpace X)

instance instLindelofSpaceSumInstTopologicalSpaceSum {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [LindelofSpace X] [LindelofSpace Y] : LindelofSpace (X ⊕ Y)

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

Equations

• (_ : LindelofSpace (X ⊕ Y)) = (_ : LindelofSpace (X ⊕ Y))

instance instLindelofSpaceSigmaInstTopologicalSpaceSigma {ι : Type u_1} {X : ι → Type u_2} [Countable ι] [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), LindelofSpace (X i)] : LindelofSpace ((i : ι) × X i)

Equations

• (_ : LindelofSpace ((i : ι) × X i)) = (_ : LindelofSpace ((i : ι) × X i))

instance Quot.LindelofSpace {X : Type u} [TopologicalSpace X] {r : X → X → Prop} [LindelofSpace X] : LindelofSpace (Quot r)

Equations

• (_ : LindelofSpace (Quot r)) = (_ : LindelofSpace (Quot r))

instance Quotient.LindelofSpace {X : Type u} [TopologicalSpace X] {s : Setoid X} [LindelofSpace X] : LindelofSpace (Quotient s)

Equations

• (_ : LindelofSpace (Quotient s)) = (_ : LindelofSpace (Quot Setoid.r))

theorem LindelofSpace.of_continuous_surjective {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} [LindelofSpace X] (hf : Continuous f) (hsur : Function.Surjective f) : LindelofSpace Y

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

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

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

• IsHereditarilyLindelof s = ∀ t ⊆ s, IsLindelof t

class HereditarilyLindelofSpace (X : Type u_2) [TopologicalSpace X] : Prop

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.

theorem IsHereditarilyLindelof.isLindelof_subset {X : Type u} [TopologicalSpace X] {s : Set X} {t : Set X} (hs : IsHereditarilyLindelof s) (ht : t ⊆ s) : IsLindelof t

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

instance HereditarilyLindelof.to_Lindelof {X : Type u} [TopologicalSpace X] [HereditarilyLindelofSpace X] : LindelofSpace X

Equations

• (_ : LindelofSpace X) = (_ : LindelofSpace X)

theorem HereditarilyLindelof_LindelofSets {X : Type u} [TopologicalSpace X] [HereditarilyLindelofSpace X] (s : Set X) : IsLindelof s

instance SecondCountableTopology.toHereditarilyLindelof {X : Type u} [TopologicalSpace X] [SecondCountableTopology X] : HereditarilyLindelofSpace X

Equations

• (_ : HereditarilyLindelofSpace X) = (_ : HereditarilyLindelofSpace X)

instance SecondCountableTopology.ofPseudoMetrizableSpaceLindelofSpace {X : Type u} [TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] [LindelofSpace X] : SecondCountableTopology X

Equations

• (_ : SecondCountableTopology X) = (_ : SecondCountableTopology X)

theorem eq_open_union_countable {X : Type u} [TopologicalSpace X] [HereditarilyLindelofSpace X] {ι : Type u} (U : ι → Set X) (h : ∀ (i : ι), IsOpen (U i)) : ∃ (t : Set ι), Set.Countable t ∧ ⋃ i ∈ t, U i = ⋃ (i : ι), U i

instance HereditarilyLindelof.lindelofSpace_subtype {X : Type u} [TopologicalSpace X] [HereditarilyLindelofSpace X] (p : X → Prop) : LindelofSpace { x : X // p x }

Equations

• (_ : LindelofSpace { x : X // p x }) = (_ : LindelofSpace ↑fun (x : X) => p x)