Theorems · Theorem · general topology

dense_iUnion_interior_of_closed

∀ {X : Type u_1} {ι : Sort u_3} [inst : TopologicalSpace X] [BaireSpace X] [Countable ι] {f : ι → Set X},
  (∀ (i : ι), IsClosed (f i)) → ⋃ i, f i = Set.univ → Dense (⋃ i, interior (f i))

Baire theorem: if countably many closed sets cover the whole space, then their interiors are dense. Formulated here with an index set which is a countable type.

Defined in

Mathlib.Topology.Baire.Lemmas

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceBaireSpaceCountable