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

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

    Instances