class PiBase.UltranormalSpace (X : Type u_1) [TopologicalSpace X] : Prop

• disjoint_clopen {s t : Set X} (st : Disjoint s t) (hs : IsClosed s) (ht : IsClosed t) : ∃ (r : Set X), IsClopen r ∧ s ⊆ r ∧ t ⊆ rᶜ