instPathConnectedSpace — Mathlib

English

ℝ is a path-connected space: for any x,y ∈ ℝ, the path γ(t)=(1−t)x+ty connects x to y.

Русский

ℝ путь-связно: для любых x,y ∈ ℝ существует путь γ(t)=(1−t)x+ty от x к y.

LaTeX

$$PathConnectedSpace ℝ$$

Lean4

/-- This is a special case of `NormedSpace.instPathConnectedSpace` (and
`IsTopologicalAddGroup.pathConnectedSpace`). It exists only to simplify dependencies. -/
instance instPathConnectedSpace : PathConnectedSpace ℝ
    where
  joined x y := ⟨⟨⟨fun (t : I) ↦ (1 - t) * x + t * y, by fun_prop⟩, by simp, by simp⟩⟩
  nonempty := inferInstance

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