reflSymmTrans — Mathlib

English

For any path p, there is a homotopy from the constant path at x1 to p.symm.trans p.

Русский

Для любой траектории p существует гомотопия от константной траектории в точке x1 к p.symm.trans p.

LaTeX

$$$\text{reflSymmTrans}(p) : \mathrm{Homotopy}(\mathrm{Path.refl}(x_1), p.symm.trans p)$$$

Lean4

/-- For any path `p` from `x₀` to `x₁`, we have a homotopy from the constant path based at `x₁` to
  `p.symm.trans p`. -/
def reflSymmTrans (p : Path x₀ x₁) : Homotopy (Path.refl x₁) (p.symm.trans p) :=
  (reflTransSymm p.symm).cast rfl <| congr_arg _ (Path.symm_symm _)

Похожие утверждения