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

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