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

• homeo_closed : ∃ (ι : Type u) (f : X → ι → ℝ), Topology.IsClosedEmbedding f