formPerm_apply_getLast — Mathlib

English

For any x and xs, formPerm (x :: xs) (getLast (x :: xs)) = x, where getLast is taken with a proof that the list is nonempty.

Русский

Для любого x и xs выполняется formPerm (x :: xs) (getLast (x :: xs)) = x, где getLast задаётся с доказательством ненулевой длины списка.

LaTeX

$$$\forall \alpha\, [\DecidableEq\ \alpha],\ \forall x:\,\alpha,\ \forall xs:\,\mathrm{List}\ \alpha,\ \mathrm{formPerm}\ (x :: xs)\ ((x :: xs).getLast\ (cons_ne_nil\ x\ xs)) = x$$$

Lean4

@[simp]
theorem formPerm_apply_getLast (x : α) (xs : List α) : formPerm (x :: xs) ((x :: xs).getLast (cons_ne_nil x xs)) = x :=
  by induction xs using List.reverseRecOn generalizing x <;> simp

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