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 #

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

    theorem SimplyConnectedSpace.paths_homotopic {X : Type u_1} [TopologicalSpace X] [SimplyConnectedSpace X] {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

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

    Another version of simply_connected_iff_paths_homotopic