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

• embeddable : ∃ (n : ℕ) (f : X → Fin n → ℝ), Topology.IsEmbedding f