Mathlib Changelog
Changelog
About
Github
Commit
2021-11-04 11:24
4c0b6ada
View on Github →
feat(topology/homotopy/basic): add
homotopic
for
continuous_map
s. (
#9865
)
Estimated changes
Modified
src/topology/homotopy/basic.lean
added
theorem
continuous_map.homotopic.equivalence
added
theorem
continuous_map.homotopic.hcomp
added
theorem
continuous_map.homotopic.refl
added
theorem
continuous_map.homotopic.symm
added
theorem
continuous_map.homotopic.trans
added
def
continuous_map.homotopic
added
theorem
continuous_map.homotopic_rel.equivalence
added
theorem
continuous_map.homotopic_rel.refl
added
theorem
continuous_map.homotopic_rel.symm
added
theorem
continuous_map.homotopic_rel.trans
added
def
continuous_map.homotopic_rel
added
theorem
continuous_map.homotopic_with.refl
added
theorem
continuous_map.homotopic_with.symm
added
theorem
continuous_map.homotopic_with.trans
added
def
continuous_map.homotopic_with
added
def
continuous_map.homotopy.hcomp
Modified
src/topology/homotopy/path.lean