snoc_injective2 — Mathlib

English

The binary function Fin.snoc is injective in both arguments.

Русский

Двойная функция Fin.snoc инъективна по обоим аргументам.

LaTeX

$$$\\mathrm{snoc\\_injective2} : \\mathrm{Function.Injective2}(\\mathrm{Fin.snoc})$$$

Lean4

/-- As a binary function, `Fin.snoc` is injective. -/
theorem snoc_injective2 : Function.Injective2 (@snoc n α) := fun x y xₙ yₙ h ↦
  ⟨funext fun i ↦ by simpa using congr_fun h (castSucc i), by simpa using congr_fun h (last n)⟩

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