English
If a countable union of closed subsets of a space covers the space, then at least one of these sets has nonempty interior.
Русский
Если счетное объединение замкнутых подмножеств пространства покрывает пространство, то по крайней мере одно из этих множеств имеет непустойInterior.
LaTeX
$$[Countable \\ ι] {f : ι → Set X} (hc : ∀ i, IsClosed (f i)) (hU : ⋃ i, f i = univ) : ∃ i, (interior f i).Nonempty$$
Lean4
/-- One of the most useful consequences of Baire theorem: if a countable union of closed sets
covers the space, then one of the sets has nonempty interior. -/
theorem nonempty_interior_of_iUnion_of_closed [Countable ι] {f : ι → Set X} (hc : ∀ i, IsClosed (f i))
(hU : ⋃ i, f i = univ) : ∃ i, (interior <| f i).Nonempty := by
simpa using (dense_iUnion_interior_of_closed hc hU).nonempty
