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

• locally_homeomorph (x : X) : ∃ U ∈ nhds x, ∃ (n : ℕ) (f : ↑U → Fin n → NNReal), Topology.IsOpenEmbedding f