Commit 2023-05-13 13:28 956490f6

View on Github →

feat: port Topology.Homotopy.Path (#3186)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Homotopy/Path.lean

added def ContinuousMap.Homotopy.evalAt

added def Path.Homotopic.Quotient.comp

added def Path.Homotopic.Quotient.mapFn

added theorem Path.Homotopic.comp_lift

added theorem Path.Homotopic.equivalence

added theorem Path.Homotopic.hcomp

added theorem Path.Homotopic.hpath_hext

added theorem Path.Homotopic.map_lift

added theorem Path.Homotopic.refl

added theorem Path.Homotopic.symm

added theorem Path.Homotopic.trans

added def Path.Homotopic

added def Path.Homotopy.cast

added theorem Path.Homotopy.coeFn_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.map

added def Path.Homotopy.refl

added def Path.Homotopy.reparam

added theorem Path.Homotopy.source

added def Path.Homotopy.symm

added theorem Path.Homotopy.symm_symm

added theorem Path.Homotopy.symm_trans

added def Path.Homotopy.symm₂

added theorem Path.Homotopy.target

added def Path.Homotopy.trans

added theorem Path.Homotopy.trans_apply