class PiBase.WellBasedSpace (X : Type u) [TopologicalSpace X] : Prop

• basis_ordered (x : X) : ∃ (ι : Type u) (s : ι → Set X), (∀ (i : ι), x ∈ s i) ∧ (nhds x).HasBasis (fun (x : ι) => True) s ∧ ∀ (i j : ι), s i ⊆ s j ∨ s j ⊆ s i