Interiors of locally closed sets

A locally closed set is nowhere dense exactly when its interior is empty (IsLocallyClosed.isNowhereDense_iff). Since finite unions of nowhere dense sets are nowhere dense, a nonempty space covered by finitely many locally closed sets has one of them with nonempty interior (TauCeti.nonempty_interior_of_iUnion_of_isLocallyClosed). This is the finite analogue of the Baire category argument nonempty_interior_of_iUnion_of_closed, valid in every topological space.

A set with empty interior need not be nowhere dense: the rationals have empty interior and are dense in the real line. They are not locally closed.

theorem IsLocallyClosed.isNowhereDense_iff {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsLocallyClosed s) : IsNowhereDense s ↔ interior s = ∅

A locally closed set is nowhere dense exactly when its interior is empty.

theorem TauCeti.nonempty_interior_of_iUnion_of_isLocallyClosed {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [Nonempty X] [Finite ι] {f : ι → Set X} (hf : ∀ (i : ι), IsLocallyClosed (f i)) (hU : ⋃ (i : ι), f i = Set.univ) : ∃ (i : ι), (interior (f i)).Nonempty

Finite covers by locally closed sets. If a nonempty space is the union of finitely many locally closed sets, one of them has nonempty interior.