mathlib documentation


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 #

structure simply_connected_space (X : Type u_1) [topological_space X] :

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

Instances of this typeclass
theorem simply_connected_space.paths_homotopic {X : Type u_1} [topological_space X] [simply_connected_space X] {x y : X} (p₁ p₂ : path x y) :
p₁.homotopic p₂

In a simply connected space, any two paths are homotopic

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} [topological_space Y] :
simply_connected_space Y path_connected_space Y ∀ {x y : Y} (p₁ p₂ : path x y), p₁.homotopic p₂

Another version of simply_connected_iff_paths_homotopic