Commit 2023-03-13 12:32 e1f0c176

View on Github →

feat: port Topology.Homotopy.Basic (#2825)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Homotopy/Basic.lean

added theorem ContinuousMap.Homotopic.equivalence

added theorem ContinuousMap.Homotopic.hcomp

added theorem ContinuousMap.Homotopic.refl

added theorem ContinuousMap.Homotopic.symm

added theorem ContinuousMap.Homotopic.trans

added def ContinuousMap.Homotopic

added theorem ContinuousMap.HomotopicRel.equivalence

added theorem ContinuousMap.HomotopicRel.refl

added theorem ContinuousMap.HomotopicRel.symm

added theorem ContinuousMap.HomotopicRel.trans

added def ContinuousMap.HomotopicRel

added theorem ContinuousMap.HomotopicWith.refl

added theorem ContinuousMap.HomotopicWith.symm

added theorem ContinuousMap.HomotopicWith.trans

added def ContinuousMap.HomotopicWith

added def ContinuousMap.Homotopy.Simps.apply

added theorem ContinuousMap.Homotopy.apply_one

added theorem ContinuousMap.Homotopy.apply_zero

added def ContinuousMap.Homotopy.cast

added theorem ContinuousMap.Homotopy.coe_toContinuousMap

added theorem ContinuousMap.Homotopy.congr_arg

added theorem ContinuousMap.Homotopy.congr_fun

added def ContinuousMap.Homotopy.curry

added theorem ContinuousMap.Homotopy.curry_apply

added theorem ContinuousMap.Homotopy.ext

added def ContinuousMap.Homotopy.extend

added theorem ContinuousMap.Homotopy.extend_apply_coe

added theorem ContinuousMap.Homotopy.extend_apply_of_le_zero

added theorem ContinuousMap.Homotopy.extend_apply_of_mem_I

added theorem ContinuousMap.Homotopy.extend_apply_of_one_le

added def ContinuousMap.Homotopy.hcomp

added def ContinuousMap.Homotopy.refl

added def ContinuousMap.Homotopy.symm

added theorem ContinuousMap.Homotopy.symm_symm

added theorem ContinuousMap.Homotopy.symm_trans

added def ContinuousMap.Homotopy.trans

added theorem ContinuousMap.Homotopy.trans_apply

added structure ContinuousMap.Homotopy

added def ContinuousMap.HomotopyRel.cast

added theorem ContinuousMap.HomotopyRel.eq_fst

added theorem ContinuousMap.HomotopyRel.eq_snd

added theorem ContinuousMap.HomotopyRel.fst_eq_snd

added def ContinuousMap.HomotopyRel.refl

added def ContinuousMap.HomotopyRel.symm

added theorem ContinuousMap.HomotopyRel.symm_symm

added theorem ContinuousMap.HomotopyRel.symm_trans

added def ContinuousMap.HomotopyRel.trans

added theorem ContinuousMap.HomotopyRel.trans_apply

added def ContinuousMap.HomotopyWith.Simps.apply

added theorem ContinuousMap.HomotopyWith.apply_one

added theorem ContinuousMap.HomotopyWith.apply_zero

added def ContinuousMap.HomotopyWith.cast

added theorem ContinuousMap.HomotopyWith.coeFn_injective

added theorem ContinuousMap.HomotopyWith.coe_toContinuousMap

added theorem ContinuousMap.HomotopyWith.coe_toHomotopy

added theorem ContinuousMap.HomotopyWith.ext

added theorem ContinuousMap.HomotopyWith.extendProp

added theorem ContinuousMap.HomotopyWith.prop

added def ContinuousMap.HomotopyWith.refl

added def ContinuousMap.HomotopyWith.symm

added theorem ContinuousMap.HomotopyWith.symm_symm

added theorem ContinuousMap.HomotopyWith.symm_trans

added def ContinuousMap.HomotopyWith.trans

added theorem ContinuousMap.HomotopyWith.trans_apply

added structure ContinuousMap.HomotopyWith