formPerm_cons_cons — Mathlib

English

For elements x,y and list l, formPerm(x :: y :: l) equals swap(x,y) times formPerm(y :: l).

Русский

Для элементов x,y и списка l формальная перестановка удовлетворяет formPerm(x :: y :: l) = swap(x,y) · formPerm(y :: l).

LaTeX

$$$\\operatorname{formPerm}(x :: y :: l) = \\operatorname{swap}(x,y) \\cdot \\operatorname{formPerm}(y :: l).$$$

Lean4

@[simp]
theorem formPerm_cons_cons (x y : α) (l : List α) : formPerm (x :: y :: l) = swap x y * formPerm (y :: l) :=
  rfl

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