Mathlib Changelog
v3
Changelog
About
Github
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