# Documentation

Mathlib.Topology.Homotopy.Contractible

# Contractible spaces #

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

def ContinuousMap.Nullhomotopic {X : Type u_1} {Y : Type u_2} [] [] (f : C(X, Y)) :

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

Instances For
theorem ContinuousMap.nullhomotopic_of_constant {X : Type u_1} {Y : Type u_2} [] [] (y : Y) :
theorem ContinuousMap.Nullhomotopic.comp_right {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : C(X, Y)} (hf : ) (g : C(Y, Z)) :
theorem ContinuousMap.Nullhomotopic.comp_left {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : C(Y, Z)} (hf : ) (g : C(X, Y)) :
class ContractibleSpace (X : Type u_1) [] :
• hequiv_unit' :

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

Instances
theorem id_nullhomotopic (X : Type u_1) [] :
theorem ContinuousMap.HomotopyEquiv.contractibleSpace {X : Type u_1} {Y : Type u_2} [] [] (e : ) :
theorem ContinuousMap.HomotopyEquiv.contractibleSpace_iff {X : Type u_1} {Y : Type u_2} [] [] (e : ) :
theorem Homeomorph.contractibleSpace {X : Type u_1} {Y : Type u_2} [] [] (e : X ≃ₜ Y) :
theorem Homeomorph.contractibleSpace_iff {X : Type u_1} {Y : Type u_2} [] [] (e : X ≃ₜ Y) :