paths_homotopic — Mathlib

English

In a simply connected space X, any two paths p1, p2 from x to y are homotopic.

Русский

В простом связном пространстве X любые две кривые-пути p1 и p2 между точками x и y гомотопичны.

LaTeX

$$$\forall X [TopologicalSpace X] [SimplyConnectedSpace X],\; \forall x,y : X,\; \forall p_1,p_2 : Path x y,\; Path.Homotopic p_1 p_2$$$

Lean4

/-- In a simply connected space, any two paths are homotopic -/
theorem paths_homotopic {x y : X} (p₁ p₂ : Path x y) : Path.Homotopic p₁ p₂ :=
  Quotient.eq.mp (@Subsingleton.elim (Path.Homotopic.Quotient x y) _ _ _)

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