Commit 2023-03-16 10:18 094cafa9

View on Github →

feat: port Topology.Homotopy.Equiv (#2919) Misc changes:

rename Homeomorph.symm_comp_to_continuousMap to Homeomorph.symm_comp_toContinuousMap;
rename Homeomorph.to_continuousMap_comp_symm to Homeomorph.toContinuousMap_comp_symm;
add CoeFun instance for Homeomorph; otherwise, toFun_eq_coe was stuck trying to coerce h to a function.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/ContinuousFunction/Basic.lean

added theorem Homeomorph.symm_comp_toContinuousMap

deleted theorem Homeomorph.symm_comp_to_continuousMap

added theorem Homeomorph.toContinuousMap_comp_symm

deleted theorem Homeomorph.to_continuousMap_comp_symm

Modified Mathlib/Topology/Homeomorph.lean

Created Mathlib/Topology/Homotopy/Equiv.lean

added def ContinuousMap.HomotopyEquiv.Simps.apply

added def ContinuousMap.HomotopyEquiv.Simps.symm_apply

added theorem ContinuousMap.HomotopyEquiv.coe_invFun

added theorem ContinuousMap.HomotopyEquiv.continuous

added def ContinuousMap.HomotopyEquiv.refl

added def ContinuousMap.HomotopyEquiv.symm

added theorem ContinuousMap.HomotopyEquiv.symm_trans

added def ContinuousMap.HomotopyEquiv.toFun'

added theorem ContinuousMap.HomotopyEquiv.toFun_eq_coe

added def ContinuousMap.HomotopyEquiv.trans

added structure ContinuousMap.HomotopyEquiv

added theorem Homeomorph.coe_toHomotopyEquiv

added theorem Homeomorph.refl_toHomotopyEquiv

added theorem Homeomorph.symm_toHomotopyEquiv

added def Homeomorph.toHomotopyEquiv

added theorem Homeomorph.trans_toHomotopyEquiv