isPathConnected — Mathlib

English

A subspace of a real topological vector space is path-connected.

Русский

Подпространство т.в. пространства над Real является путепроходимым.

LaTeX

$$$ \text{IsPathConnected}((s:\,Submodule\;\mathbb{R}\;E) : \text{Set }E) $$$

Lean4

/-- A subspace in a topological vector space over `ℝ` is path connected. -/
theorem isPathConnected (s : Submodule ℝ E) : IsPathConnected (s : Set E) :=
  s.convex.isPathConnected s.nonempty

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