simply_connected_iff_paths_homotopic'

English

A space Y is simply connected iff it is path-connected and for any endpoints x,y and any paths p1,p2 : Path x y, we have p1 homotopic to p2.

Русский

Пространство Y просто связно тогда и только тогда, когда оно связано по путям и для любых концовых точек x,y и любых путей p1,p2 : Path x y выполняется p1 гомотопично p2.

LaTeX

$$$\text{SimplyConnectedSpace } Y \iff \text{PathConnectedSpace } Y \land \forall {x y : Y} (p_1 p_2 : Path x y), Path.Homotopic p_1 p_2$$$

Lean4

/-- Another version of `simply_connected_iff_paths_homotopic` -/
theorem simply_connected_iff_paths_homotopic' {Y : Type*} [TopologicalSpace Y] :
    SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ {x y : Y} (p₁ p₂ : Path x y), Path.Homotopic p₁ p₂ :=
  by
  convert simply_connected_iff_paths_homotopic (Y := Y)
  simp [Path.Homotopic.Quotient, Setoid.eq_top_iff]; rfl

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