# 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) [] :

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

• equiv_unit :
Instances
theorem SimplyConnectedSpace.equiv_unit {X : Type u_1} [] [self : ] :
theorem simply_connected_iff_unique_homotopic (X : Type u_1) [] :
∀ (x y : X),
instance SimplyConnectedSpace.instSubsingletonQuotient {X : Type u_1} [] (x : X) (y : X) :
Equations
• =
@[instance 100]
Equations
• =
theorem SimplyConnectedSpace.paths_homotopic {X : Type u_1} [] {x : X} {y : X} (p₁ : Path x y) (p₂ : Path x y) :
p₁.Homotopic p₂

In a simply connected space, any two paths are homotopic

@[instance 100]
Equations
• =
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), p₁.Homotopic p₂

Another version of simply_connected_iff_paths_homotopic