snoc_inj — Mathlib

English

Snoc is injective in the sense that Eq (Fin.snoc x x_n) (Fin.snoc y y_n) implies x = y and x_n = y_n.

Русский

Snoc-инъективно: если равны результаты snoc с соответствующими аргументами, то аргументы равны по компонентам.

LaTeX

$$$\\mathrm{snoc\\_inj} : \\forall x\\ y\\ x_n\\ y_n, \\mathrm{snoc} x x_n = \\mathrm{snoc} y y_n \\Rightarrow x = y \\land x_n = y_n$$$

Lean4

@[simp]
theorem snoc_inj {x y : ∀ i : Fin n, α i.castSucc} {xₙ yₙ : α (last n)} : snoc x xₙ = snoc y yₙ ↔ x = y ∧ xₙ = yₙ :=
  snoc_injective2.eq_iff

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