sym2_map — Mathlib

English

Mapping a function over a list commutes with the construction of Sym2, i.e., (xs.map f).sym2 = xs.sym2.map (Sym2.map f).

Русский

Построение Sym2 тогда и только тогда, когда применяется отображение к списку и затем к Sym2, совпадает: (xs.map f).sym2 = xs.sym2.map (Sym2.map f).

LaTeX

$$$$ (\\mathrm{xs.map}\\; f).\\mathrm{sym2} = \\mathrm{xs}.\\mathrm{sym2}.map(\\mathrm{Sym2.map}\\; f) $$$$

Lean4

theorem sym2_map (f : α → β) (xs : List α) : (xs.map f).sym2 = xs.sym2.map (Sym2.map f) := by
  induction xs with
  | nil => simp [List.sym2]
  | cons x xs ih => simp [List.sym2, ih, Function.comp]

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