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

• locally_homeomorph : ∃ (n : ℕ), ∀ (x : X), ∃ s ∈ nhds x, Nonempty (↑s ≃ₜ (Fin n → ℝ))