transRefl — Mathlib

English

The transRefl map provides a homotopy from p.trans (refl x1) to p.

Русский

transRefl отображение задаёт гомотопию от p.trans (refl x1) к p.

LaTeX

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

Lean4

/-- For any path `p` from `x₀` to `x₁`, we have a homotopy from `p.trans (Path.refl x₁)` to `p`. -/
def transRefl (p : Path x₀ x₁) : Homotopy (p.trans (Path.refl x₁)) p :=
  ((Homotopy.reparam p (fun t => ⟨transReflReparamAux t, transReflReparamAux_mem_I t⟩) (by fun_prop)
          (Subtype.ext transReflReparamAux_zero) (Subtype.ext transReflReparamAux_one)).cast
      rfl (trans_refl_reparam p).symm).symm

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