snoc_castAdd — Mathlib

English

snoc is injective in both arguments: 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\\ Injective2}\\ (x,y) : \\mathrm{snoc}\\ x\\ x_n = \\mathrm{snoc}\\ y\\ y_n \\Rightarrow x = y \\land x_n = y_n$$$

Lean4

@[simp]
theorem snoc_castAdd {α : Fin (n + m + 1) → Sort*} (f : ∀ i : Fin (n + m), α i.castSucc) (a : α (last (n + m)))
    (i : Fin n) : (snoc f a) (castAdd (m + 1) i) = f (castAdd m i) :=
  dif_pos _

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