Theorems · Theorem · general topology

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

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

Defined in

Mathlib.Topology.Compactness.Lindelof

Cited by

10 results in Mathlib

Foundations

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

Assumes

TopologicalSpace