instPathConnectedSpace — Mathlib

English

If X is simply connected, then X is path-connected: for any x,y in X there exists a path from x to y.

Русский

Если X являетсяSimplyConnected, то X является связным по путям: для любых x,y из X существует путь от x до y.

LaTeX

$$$\forall x,y \in X, \exists p : Path x y$$$

Lean4

instance (priority := 100) : PathConnectedSpace X :=
  let unique_homotopic := (simply_connected_iff_unique_homotopic X).mp inferInstance
  { nonempty := unique_homotopic.1
    joined := fun x y => ⟨(unique_homotopic.2 x y).some.default.out⟩ }

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