Commit 2021-10-11 20:04 136d0ce9

View on Github →

feat(topology/homotopy/path): Add homotopy between paths (#9141) There is also a lemma about path.to_continuous_map which I needed in a prior iteration of this PR that I missed in #9133

Estimated changes

Modified src/topology/homotopy/basic.lean

Created src/topology/homotopy/path.lean

added theorem path.homotopic.equivalence

added theorem path.homotopic.refl

added theorem path.homotopic.symm

added theorem path.homotopic.trans

added def path.homotopic

added theorem path.homotopy.coe_fn_injective

added def path.homotopy.eval

added theorem path.homotopy.eval_one

added theorem path.homotopy.eval_zero

added def path.homotopy.hcomp

added theorem path.homotopy.hcomp_apply

added theorem path.homotopy.hcomp_half

added def path.homotopy.refl

added theorem path.homotopy.source

added def path.homotopy.symm

added theorem path.homotopy.symm_symm

added theorem path.homotopy.symm_trans

added theorem path.homotopy.target

added def path.homotopy.trans

added theorem path.homotopy.trans_apply

added def path.homotopy

Modified src/topology/path_connected.lean

added theorem path.coe_to_continuous_map