Abstract
In complex analysis, one often has to manipulate paths, i.e. curves in the complex plane. This entry defines three useful relations on paths:
- an equivalence relation $\equiv_{\text{p}}$ that describes that two paths are the same up to reparametrisation
- a preorder $\leq_{\text{p}}$ that expresses the notion that one path is a subpath of another
- an equivalence relation $\equiv_{\bigcirc}$ that describes equivalence of closed paths up to reparametrisation and “shifting” (e.g. if we have a rectangular path, it does not matter which corner we start in)
It also provides the path tactic, which proves or simplifies some common proof obligations for composite paths. Namely:
- proving $\equiv_{\text{p}}$, $\leq_{\text{p}}$, $\equiv_{\bigcirc}$
- proving well-definedness of paths (path, valid_path)
- determining the image of a path (path_image)
- showing that a path is not self-intersecting (arc, simple_path)
- decomposing integrals on a composite path into the integrals on the constituent paths