snoc_comp_castAdd — Mathlib

English

snoc is injective in the left argument and last coordinate, i.e., if snoc x x_n = snoc y y_n then x=y and x_n=y_n.

Русский

snoc инъективен по левому аргументу и последней координате: если snoc x x_n = snoc y y_n, то x=y и x_n=y_n.

LaTeX

$$$\\mathrm{snoc\\ inj} : \\forall x,y\\,\\; snoc x = snoc y \\Rightarrow x=y$$$

Lean4

@[simp]
theorem snoc_comp_castAdd {n m : ℕ} {α : Sort*} (f : Fin (n + m) → α) (a : α) :
    (snoc f a : Fin _ → α) ∘ castAdd (m + 1) = f ∘ castAdd m :=
  funext (snoc_castAdd _ _)

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