isPathConnected — Mathlib

English

A nonempty convex set is path-connected.

Русский

Непустое выпуклое множество является связным по пути.

LaTeX

$$$ \text{Convex}(s) \land s \neq \emptyset \Rightarrow \text{IsPathConnected}(s) $$$

Lean4

/-- A nonempty convex set is path connected. -/
protected theorem isPathConnected {s : Set E} (hconv : Convex ℝ s) (hne : s.Nonempty) : IsPathConnected s :=
  let ⟨_a, ha⟩ := hne;
  (hconv ha).isPathConnected ha

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