delayReflRight_zero — Mathlib

English

For any path γ, delayReflRight(0, γ) equals γ concatenated with the constant path at its endpoint y.

Русский

Для любого пути γ, delayReflRight(0, γ) равен γ, далее соединенному с константным путём в точке y.

LaTeX

$$delayReflRight(0, γ) = γ.trans (refl y)$$

Lean4

theorem delayReflRight_zero (γ : Path x y) : delayReflRight 0 γ = γ.trans (Path.refl y) :=
  by
  ext t
  simp only [delayReflRight, trans_apply, Path.coe_mk_mk, refl_apply]
  split_ifs with h; swap
  on_goal 1 => conv_rhs => rw [← γ.target]
  all_goals apply congr_arg γ; ext1; rw [qRight_zero_right]
  exacts [if_neg h, if_pos h]

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