contractibleSpace — Mathlib

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

Похожие утверждения