permutationsAux2_snd_nil — Mathlib

English

If the input to permutationsAux2 is (y :: ys), the second component is f (t :: y :: ys ++ ts) :: permutationsAux2 t ts r ys (fun x => f (y :: x)).2.

Русский

Если ввод в permutationsAux2 равен (y :: ys), то вторая компонента равна f (t :: y :: ys ++ ts) :: permutationsAux2 t ts r ys (fun x => f (y :: x)).2.

LaTeX

$$$(permutationsAux2\ t\ ts\ r\ (y::ys)\ f).2 = f (t :: y :: ys ++ ts) :: (permutationsAux2\ t\ ts\ r\ ys\ (\lambda x. f (y :: x))).2$$$

Lean4

@[simp]
theorem permutationsAux2_snd_nil (t : α) (ts : List α) (r : List β) (f : List α → β) :
    (permutationsAux2 t ts r [] f).2 = r :=
  rfl

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