English
A space Y is simply connected iff it is path-connected and between any two points there is at most one homotopy class of paths.
Русский
Пространство Y просто связно тогда и только тогда, когда оно связано по путям и между любыми двумя точками существует не более одного класса путей по гомотопии.
LaTeX
$$$\text{SimplyConnectedSpace } Y \iff \text{PathConnectedSpace } Y \land \forall x,y : Y,\; \Subsingleton (Path.Homotopic.Quotient x y)$$$
Lean4
/-- A space is simply connected iff it is path connected, and there is at most one path
up to homotopy between any two points. -/
theorem simply_connected_iff_paths_homotopic {Y : Type*} [TopologicalSpace Y] :
SimplyConnectedSpace Y ↔ PathConnectedSpace Y ∧ ∀ x y : Y, Subsingleton (Path.Homotopic.Quotient x y) :=
⟨by intro; constructor <;> infer_instance, fun h => by
cases h; rw [simply_connected_iff_unique_homotopic]
exact ⟨inferInstance, fun x y => ⟨uniqueOfSubsingleton ⟦PathConnectedSpace.somePath x y⟧⟩⟩⟩
