theorem interior_closure_iInter_eq_interior_iInter_closure_of_isOpen {X : Type u} [TopologicalSpace X] [BaireSpace X] (U : ℕ → Set X) (hopen : ∀ (n : ℕ), IsOpen (U n)) : interior (closure (⋂ (n : ℕ), U n)) = interior (⋂ (n : ℕ), closure (U n))

Baire-space form of the corrected open-set clause used in Lemma 1.44: for a countable family of open sets, taking the interior after the closure of the intersection agrees with taking the interior after intersecting the closures.

theorem closure_iUnion_interior_eq_closure_interior_iUnion_of_isClosed {X : Type u} [TopologicalSpace X] [BaireSpace X] (C : ℕ → Set X) (hclosed : ∀ (n : ℕ), IsClosed (C n)) : closure (⋃ (n : ℕ), interior (C n)) = closure (interior (⋃ (n : ℕ), C n))

Baire-space form of the corrected closed-set clause used in Lemma 1.44, dual to interior_closure_iInter_eq_interior_iInter_closure_of_isOpen.

theorem lemma_1_44 {X : Type u} [MetricSpace X] [CompleteSpace X] : (∀ (C : ℕ → Set X), (∀ (n : ℕ), IsClosed (C n)) → closure (⋃ (n : ℕ), interior (C n)) = closure (interior (⋃ (n : ℕ), C n))) ∧ ∀ (U : ℕ → Set X), (∀ (n : ℕ), IsOpen (U n)) → interior (closure (⋂ (n : ℕ), U n)) = interior (⋂ (n : ℕ), closure (U n))

Lemma 1.44 [Ursescu]: specialized to complete metric spaces through their canonical BaireSpace instance, the corrected Baire-category identities for countable unions of closed sets and countable intersections of open sets hold with the necessary closure operators.