# mathlibdocumentation

algebraic_topology.fundamental_groupoid.simply_connected

# 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

• simply_connected_space.of_contractible - A contractible space is simply connected

@[class]
structure simply_connected_space (X : Type u_1)  :
Prop
• equiv_unit :

A simply connected space is one whose fundamental groupoid is equivalent to discrete unit

Instances of this typeclass
theorem simply_connected_def (X : Type u_1)  :
theorem simply_connected_iff_unique_homotopic (X : Type u_1)  :
∀ (x y : X),
@[protected, instance]
@[protected, instance]
theorem simply_connected_space.paths_homotopic {X : Type u_1} {x y : X} (p₁ p₂ : path x y) :
p₁.homotopic p₂

In a simply connected space, any two paths are homotopic

@[protected, instance]
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