mathlib3 documentation

topology.homotopy.contractible

Contractible spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [topological_space X] [topological_space Y] (f : C(X, Y)) :
Prop

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

Equations
theorem continuous_map.nullhomotopic.comp_right {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [topological_space X] [topological_space Y] [topological_space Z] {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} [topological_space X] [topological_space Y] [topological_space Z] {f : C(Y, Z)} (hf : f.nullhomotopic) (g : C(X, Y)) :
@[class]
structure contractible_space (X : Type u_1) [topological_space X] :
Prop

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

Instances of this typeclass