pathConnectedSpace — Mathlib

English

Every real topological vector space is path-connected.

Русский

Каждое топологическое векторное пространство над Real является путепроходимым.

LaTeX

$$$ \text{PathConnected}\;E $ for any topological vector space $E$ over $\mathbb{R}$.$$

Lean4

/-- Every topological vector space over ℝ is path connected.

Not an instance, because it creates enormous TC subproblems (turn on `pp.all`).
-/
protected theorem pathConnectedSpace : PathConnectedSpace E :=
  pathConnectedSpace_iff_univ.mpr <| convex_univ.isPathConnected ⟨(0 : E), trivial⟩

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