class PiBase.FullyT4Space (X : Type u_1) [TopologicalSpace X] extends T1Space X, PiBase.FullyNormalSpace X : Prop

• t1 (x : X) : IsClosed {x}
• locallyFinite_refinement (α : Type u_1) (s : α → Set X) : (∀ (a : α), IsOpen (s a)) → ⋃ (a : α), s a = Set.univ → ∃ (β : Type u_1) (t : β → Set X), (∀ (b : β), IsOpen (t b)) ∧ ⋃ (b : β), t b = Set.univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ (a : α), t b ⊆ s a
• normal (s t : Set X) : IsClosed s → IsClosed t → Disjoint s t → SeparatedNhds s t