Documentation

Mathlib.Topology.Homotopy.Contractible

Contractible spaces #

In this file, we define ContractibleSpace, a space that is homotopy equivalent to Unit.

A map is nullhomotopic if it is homotopic to a constant map.

Equations
Instances For
    theorem ContinuousMap.nullhomotopic_of_constant {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (y : Y) :
    (ContinuousMap.const X y).Nullhomotopic
    theorem ContinuousMap.Nullhomotopic.comp_right {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(X, Y)} (hf : f.Nullhomotopic) (g : C(Y, Z)) :
    (g.comp f).Nullhomotopic
    theorem ContinuousMap.Nullhomotopic.comp_left {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : C(Y, Z)} (hf : f.Nullhomotopic) (g : C(X, Y)) :
    (f.comp g).Nullhomotopic

    A contractible space is one that is homotopy equivalent to Unit.

    Instances