Commit 2023-05-14 11:05 adf58592

View on Github →

feat: port Topology.Homotopy.Contractible (#3960)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Homotopy/Contractible.lean

added theorem ContinuousMap.Nullhomotopic.comp_left

added theorem ContinuousMap.Nullhomotopic.comp_right

added def ContinuousMap.Nullhomotopic

added theorem ContinuousMap.nullhomotopic_of_constant

added theorem ContractibleSpace.hequiv_unit

added theorem contractible_iff_id_nullhomotopic

added theorem id_nullhomotopic