Mathlib Changelog
v4
Changelog
About
Github
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