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