# mathlibdocumentation

topology.homotopy.contractible

# Contractible spaces #

In this file, we define contractible_space, a space that is homotopy equivalent to unit.

def continuous_map.nullhomotopic {X : Type u_1} {Y : Type u_2} (f : C(X, Y)) :
Prop

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

Equations
theorem continuous_map.nullhomotopic_of_constant {X : Type u_1} {Y : Type u_2} (y : Y) :
theorem continuous_map.nullhomotopic.comp_right {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : C(X, Y)} (hf : f.nullhomotopic) (g : C(Y, Z)) :
theorem continuous_map.nullhomotopic.comp_left {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : C(Y, Z)} (hf : f.nullhomotopic) (g : C(X, Y)) :
@[class]
structure contractible_space (X : Type u_1)  :
Prop
• hequiv_unit :

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

Instances of this typeclass
theorem id_nullhomotopic (X : Type u_1)  :
theorem contractible_iff_id_nullhomotopic (Y : Type u_1)  :
@[protected]
theorem continuous_map.homotopy_equiv.contractible_space {X : Type u_1} {Y : Type u_2} (e : Y) :
@[protected]
theorem continuous_map.homotopy_equiv.contractible_space_iff {X : Type u_1} {Y : Type u_2} (e : Y) :
@[protected]
theorem homeomorph.contractible_space {X : Type u_1} {Y : Type u_2} (e : X ≃ₜ Y) :
@[protected]
theorem homeomorph.contractible_space_iff {X : Type u_1} {Y : Type u_2} (e : X ≃ₜ Y) :
@[protected, instance]