Commit 2023-04-17 10:44 35acfaa7

View on Github →

feat: use HomotopyLike for HomotopyWith (#3197) Also fix some simp/simps.

Estimated changes

Modified Mathlib/Topology/Homotopy/Basic.lean

modified def ContinuousMap.HomotopyRel.symm

modified def ContinuousMap.HomotopyWith.Simps.apply

modified theorem ContinuousMap.HomotopyWith.coeFn_injective

modified theorem ContinuousMap.HomotopyWith.ext

modified theorem ContinuousMap.HomotopyWith.extendProp

modified def ContinuousMap.HomotopyWith.refl

modified def ContinuousMap.HomotopyWith.symm