Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-12 23:00 7ece83ed

View on Github →

feat(topology/homotopy): Add definition of contractible spaces (#12731)

Estimated changes

Created src/topology/homotopy/contractible.lean

added theorem continuous_map.nullhomotopic.comp_left

added theorem continuous_map.nullhomotopic.comp_right

added def continuous_map.nullhomotopic

added theorem continuous_map.nullhomotopic_of_constant

added theorem contractible_iff_id_nullhomotopic

added theorem id_nullhomotopic