Theorems · Theorem · general topology

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

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

Defined in

Mathlib.Topology.Compactness.Lindelof

Cited by

4 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace