formPerm_append_pair — Mathlib

English

The formPerm permutation of a list reversed equals the inverse of formPerm of the original list.

Русский

Перестановка formPerm от списка в обратном порядке равна обратной перестановке formPerm исходного списка.

LaTeX

$$$\forall \alpha\,[\DecidableEq\alpha],\ \forall l:\,\mathrm{List}\ \alpha,\ \mathrm{formPerm}\ l\ \mathrm{reverse}=\big(\mathrm{formPerm}\ l\big)^{-1}$$$

Lean4

theorem formPerm_append_pair : ∀ (l : List α) (a b : α), formPerm (l ++ [a, b]) = formPerm (l ++ [a]) * swap a b
  | [], _, _ => rfl
  | [_], _, _ => rfl
  | x :: y :: l, a, b => by simpa [mul_assoc] using formPerm_append_pair (y :: l) a b

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