Theorems · Theorem · general topology

IsLindelof.indexed_countable_subcover

∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {ι : Type v} [Nonempty ι],
  IsLindelof s → ∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → 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 ℕ.

Defined in

Mathlib.Topology.Compactness.Lindelof

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNonempty