Theorems · Theorem · general topology

dense_biUnion_interior_of_closed

∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [BaireSpace X] {S : Set α} {f : α → Set X},
  (∀ s ∈ S, IsClosed (f s)) → S.Countable → ⋃ s ∈ S, f s = Set.univ → Dense (⋃ s ∈ S, interior (f s))

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 set in any type.

Defined in

Mathlib.Topology.Baire.Lemmas

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceBaireSpace