English
Let X be a topological space that is a Baire space. If {f_i}_{i∈ι} is a countable family of closed subsets of X whose union is the whole space, then the union of their interiors is dense in X.
Русский
Пусть X — топологическое пространство, являющееся пространством Бэра. Пусть {f_i}_{i∈ι} — счетное семейство замкнутых подмножеств X, чьё объединение равно X. Тогда объединение ихInterior плотно в X.
LaTeX
$$$[Countable \\ ι] \\quad {f : ι \\to \\mathcal P(X)}\\ \\bigl( \\forall i, IsClosed(f(i)) \\bigr) \\land \\bigl( \\bigcup_i f(i) = \\mathsf{univ} \\bigr) \\Rightarrow Dense\\left( \\bigcup_i \\operatorname{int}(f(i)) \\right)$$
Lean4
/-- 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. -/
theorem dense_iUnion_interior_of_closed [Countable ι] {f : ι → Set X} (hc : ∀ i, IsClosed (f i))
(hU : ⋃ i, f i = univ) : Dense (⋃ i, interior (f i)) :=
IsGδ.univ.dense_iUnion_interior_of_closed dense_univ hc hU.ge
