mathlib3 documentation

algebraic_topology.fundamental_groupoid.simply_connected

Simply connected spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines simply connected spaces. A topological space is simply connected if its fundamental groupoid is equivalent to unit.

Main theorems #

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

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.