Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-01-07 18:21
3b02ad77
View on Github →
feat(topology/homotopy/equiv): Add homotopy equivalences between topological spaces (
#10529
)
Estimated changes
Modified
src/topology/continuous_function/basic.lean
added
theorem
continuous_map.comp_id
added
theorem
continuous_map.id_comp
Created
src/topology/homotopy/equiv.lean
added
theorem
continuous_map.homotopy_equiv.coe_inv_fun
added
theorem
continuous_map.homotopy_equiv.continuous
added
def
continuous_map.homotopy_equiv.refl
added
def
continuous_map.homotopy_equiv.simps.apply
added
def
continuous_map.homotopy_equiv.simps.symm_apply
added
def
continuous_map.homotopy_equiv.symm
added
theorem
continuous_map.homotopy_equiv.symm_trans
added
theorem
continuous_map.homotopy_equiv.to_fun_eq_coe
added
def
continuous_map.homotopy_equiv.trans
added
structure
continuous_map.homotopy_equiv
added
theorem
homeomorph.coe_to_homotopy_equiv
added
theorem
homeomorph.refl_to_homotopy_equiv
added
theorem
homeomorph.symm_to_homotopy_equiv
added
def
homeomorph.to_homotopy_equiv
added
theorem
homeomorph.trans_to_homotopy_equiv