class PiBase.TopologicalNManifold (X : Type u) [TopologicalSpace X] extends PiBase.LocallyNEuclideanSpace X, T2Space X, SecondCountableTopology X : Prop

• locally_homeomorph : ∃ (n : ℕ), ∀ (x : X), ∃ s ∈ nhds x, Nonempty (↑s ≃ₜ (Fin n → ℝ))
• t2 : Pairwise fun (x y : X) => ∃ (u : Set X) (v : Set X), IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
• is_open_generated_countable : ∃ (b : Set (Set X)), b.Countable ∧ inst✝ = TopologicalSpace.generateFrom b