English
Every real topological vector space is contractible; there is a continuous deformation moving all points to any fixed origin within the space.
Русский
Каждое вещественное топологическое векторное пространство контрактно; существует непрерывная деформация, переводящая все точки в фиксированную точку внутри пространства.
LaTeX
$$$$\\text{ContractibleSpace}(E)\\quad \\text{for any real topological vector space } E.$$$$
Lean4
instance (priority := 100) contractibleSpace : ContractibleSpace E :=
(Homeomorph.Set.univ E).contractibleSpace_iff.mp <| convex_univ.contractibleSpace Set.univ_nonempty