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

• homeomorphic_to_tvs : ∃ (a : AddCommMonoid X) (x : Module ℝ X), (Continuous fun (x_1 : ℝ × X) => match x_1 with | (r, x_2) => r • x_2) ∧ Continuous fun (x : X × X) => match x with | (x, y) => x + y