Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-04 11:24 4c0b6ada

View on Github →

feat(topology/homotopy/basic): add homotopic for continuous_maps. (#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