formPerm_cons_concat_apply_last — Mathlib

English

For any x, y and any xs, the permutation formPerm (x :: (xs ++ [y])) sends y to x.

Русский

Для любых элементов x, y и списка xs перестановка formPerm (x :: (xs ++ [y])) отображает y в x.

LaTeX

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

Lean4

@[simp]
theorem formPerm_cons_concat_apply_last (x y : α) (xs : List α) : formPerm (x :: (xs ++ [y])) y = x := by
  induction xs generalizing x y with
  | nil => simp
  | cons z xs IH => simp [IH]

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