permutationsAux2_snd_cons — Mathlib

English

Appending the result of permutationsAux2 with an extra r is the same as permuting with r appended on the right; formalizes a right-extension property of the construction.

Русский

Дополнение результата permutationsAux2 дополнительным r эквивалентно перестановке с r, добавленным справа.

LaTeX

$$$(permutationsAux2\ t\ ts\ nil\ ys\ f).2 \;++\; r = (permutationsAux2\ t\ ts\ r\ ys\ f).2$$$

Lean4

@[simp]
theorem permutationsAux2_snd_cons (t : α) (ts : List α) (r : List β) (y : α) (ys : List α) (f : List α → β) :
    (permutationsAux2 t ts r (y :: ys) f).2 =
      f (t :: y :: ys ++ ts) :: (permutationsAux2 t ts r ys fun x : List α => f (y :: x)).2 :=
  by simp [permutationsAux2, permutationsAux2_fst t _ _ ys]

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