class PiBase.MonotonicallyNormalSpace (X : Type u_1) [TopologicalSpace X] extends T1Space X : Prop

• t1 (x : X) : IsClosed {x}
• monotonically_normal : ∃ (μ : (x : X) → (s : TopologicalSpace.Opens X) → x ∈ s → TopologicalSpace.Opens X), ∀ (x : X) (s : TopologicalSpace.Opens X) (hs : x ∈ s), x ∈ μ x s hs ∧ ∀ (x y : X) (u v : TopologicalSpace.Opens X) (hu : x ∈ u) (hv : y ∈ v), ↑(μ x u hu) ∩ ↑(μ y v hv) ≠ ∅ → x ∈ v ∨ y ∈ u