map_permutationsAux2 — Mathlib

English

When r = [] the map argument can be eliminated from permutationsAux2.

Русский

Если r = [], отображение может быть устранено из permutationsAux2.

LaTeX

$$$(permutationsAux2\ t\ ts\ []\ ys\ id).2.map\ f = (permutationsAux2\ t\ ts\ []\ ys\ f).2$$$

Lean4

/-- The `f` argument to `permutationsAux2` when `r = []` can be eliminated. -/
theorem map_permutationsAux2 (t : α) (ts : List α) (ys : List α) (f : List α → β) :
    (permutationsAux2 t ts [] ys id).2.map f = (permutationsAux2 t ts [] ys f).2 :=
  by
  rw [map_permutationsAux2' id, map_id, map_id]
  · rfl
  simp

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