# Documentation

Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

# Simply connected spaces #

This file defines simply connected spaces. A topological space is simply connected if its fundamental groupoid is equivalent to Unit.

## Main theorems #

• simply_connected_iff_unique_homotopic - A space is simply connected if and only if it is nonempty and there is a unique path up to homotopy between any two points

• SimplyConnectedSpace.ofContractible - A contractible space is simply connected

theorem simply_connected_def (X : Type u_1) [] :
class SimplyConnectedSpace (X : Type u_1) [] :
• equiv_unit :

A simply connected space is one whose fundamental groupoid is equivalent to Discrete Unit

Instances
theorem simply_connected_iff_unique_homotopic (X : Type u_1) [] :
∀ (x y : X),
instance SimplyConnectedSpace.instSubsingletonQuotient {X : Type u_1} [] (x : X) (y : X) :
theorem SimplyConnectedSpace.paths_homotopic {X : Type u_1} [] {x : X} {y : X} (p₁ : Path x y) (p₂ : Path x y) :
Path.Homotopic p₁ p₂

In a simply connected space, any two paths are homotopic

theorem simply_connected_iff_paths_homotopic {Y : Type u_1} [] :
∀ (x y : Y),

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 u_1} [] :
∀ {x y : Y} (p₁ p₂ : Path x y), Path.Homotopic p₁ p₂

Another version of simply_connected_iff_paths_homotopic