Theorems · Theorem · general topology

eq_open_union_countable

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

Defined in

Mathlib.Topology.Compactness.Lindelof

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceHereditarilyLindelofSpace