Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-04 15:09 387ff6e3

View on Github →

feat(topology/homotopy): add homotopy_with (#9252) Added homotopy_with as in HOL-Analysis extending homotopy. Furthermore, I've added homotopy_rel. Also rename/moved the file. There is also some refactoring which is part of the suggestions from #9141 .

Estimated changes

Deleted src/topology/homotopy.lean

deleted theorem continuous_map.homotopy.apply_one

deleted theorem continuous_map.homotopy.apply_zero

deleted def continuous_map.homotopy.curry

deleted theorem continuous_map.homotopy.ext

deleted def continuous_map.homotopy.extend

deleted theorem continuous_map.homotopy.extend_apply_one

deleted theorem continuous_map.homotopy.extend_apply_zero

deleted def continuous_map.homotopy.refl

deleted def continuous_map.homotopy.symm

deleted theorem continuous_map.homotopy.symm_apply

deleted theorem continuous_map.homotopy.symm_symm

deleted theorem continuous_map.homotopy.symm_trans

deleted theorem continuous_map.homotopy.to_continuous_map_apply

deleted def continuous_map.homotopy.trans

deleted theorem continuous_map.homotopy.trans_apply

deleted structure continuous_map.homotopy

Created src/topology/homotopy/basic.lean

added theorem continuous_map.homotopy.apply_one

added theorem continuous_map.homotopy.apply_zero

added theorem continuous_map.homotopy.coe_fn_injective

added theorem continuous_map.homotopy.coe_to_continuous_map

added theorem continuous_map.homotopy.congr_arg

added theorem continuous_map.homotopy.congr_fun

added def continuous_map.homotopy.curry

added theorem continuous_map.homotopy.curry_apply

added theorem continuous_map.homotopy.ext

added def continuous_map.homotopy.extend

added theorem continuous_map.homotopy.extend_apply_coe

added theorem continuous_map.homotopy.extend_apply_of_le_zero

added theorem continuous_map.homotopy.extend_apply_of_mem_I

added theorem continuous_map.homotopy.extend_apply_of_one_le

added def continuous_map.homotopy.refl

added def continuous_map.homotopy.simps.apply

added def continuous_map.homotopy.symm

added theorem continuous_map.homotopy.symm_symm

added theorem continuous_map.homotopy.symm_trans

added def continuous_map.homotopy.trans

added theorem continuous_map.homotopy.trans_apply

added structure continuous_map.homotopy

added theorem continuous_map.homotopy_rel.eq_fst

added theorem continuous_map.homotopy_rel.eq_snd

added theorem continuous_map.homotopy_rel.fst_eq_snd

added def continuous_map.homotopy_rel.refl

added def continuous_map.homotopy_rel.symm

added theorem continuous_map.homotopy_rel.symm_symm

added theorem continuous_map.homotopy_rel.symm_trans

added def continuous_map.homotopy_rel.trans

added theorem continuous_map.homotopy_rel.trans_apply

added def continuous_map.homotopy_rel

added theorem continuous_map.homotopy_with.apply_one

added theorem continuous_map.homotopy_with.apply_zero

added theorem continuous_map.homotopy_with.coe_fn_injective

added theorem continuous_map.homotopy_with.coe_to_continuous_map

added theorem continuous_map.homotopy_with.coe_to_homotopy

added theorem continuous_map.homotopy_with.ext

added theorem continuous_map.homotopy_with.extend_prop

added theorem continuous_map.homotopy_with.prop

added def continuous_map.homotopy_with.refl

added def continuous_map.homotopy_with.simps.apply

added def continuous_map.homotopy_with.symm

added theorem continuous_map.homotopy_with.symm_symm

added theorem continuous_map.homotopy_with.symm_trans

added def continuous_map.homotopy_with.trans

added theorem continuous_map.homotopy_with.trans_apply

added structure continuous_map.homotopy_with