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

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