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

• locally_homeomorph (x : X) : ∃ s ∈ nhds x, ∃ (f : ↑s → NNReal), Topology.IsOpenEmbedding f