theorem BaireCategory.baire_category_theorem {M : Type u_1} [MetricSpace M] [CompleteSpace M] [Nonempty M] {C : ℕ → Set M} (hc : ∀ (n : ℕ), IsClosed (C n)) (hU : ⋃ (n : ℕ), C n = Set.univ) : ∃ (n : ℕ), (interior (C n)).Nonempty

Baire Category Theorem. Let $M$ be a (nonempty) complete metric space, and let $\{C_n\}_{n \in \mathbb{N}}$ be a collection of closed subsets of $M$ such that $M = \bigcup_{n \in \mathbb{N}} C_n$. Then at least one of the $C_n$ has nonempty interior, i.e. contains an open ball $B(x, r) = \{y \in M : d(x, y) < r\}$.