formPerm_apply_getElem_length — Mathlib

English

For any x and xs, formPerm (x :: xs) (x :: xs)[xs.length] = x.

Русский

Для любого x и xs выполняется formPerm (x :: xs) (x :: xs)[xs.length] = x.

LaTeX

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

Lean4

@[simp]
theorem formPerm_apply_getElem_length (x : α) (xs : List α) : formPerm (x :: xs) (x :: xs)[xs.length] = x := by
  rw [getElem_cons_length rfl, formPerm_apply_getLast]

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