fold_cons — Mathlib

English

If a is not in s, then folding over cons a s equals op(f(a), fold op b f s).

Русский

Если a не принадлежит s, то свёртка по (cons a s) равна op(f(a), fold op b f s).

LaTeX

$$$\\mathrm{fold}_{op}\\; b\\; f\\; (\\mathrm{cons}\\ a\\ s\\ h) = op(f(a), \\mathrm{fold}_{op}\\; b\\; f\\; s)$$$

Lean4

@[simp]
theorem fold_cons (h : a ∉ s) : (cons a s h).fold op b f = f a * s.fold op b f :=
  by
  dsimp only [fold]
  rw [cons_val, Multiset.map_cons, fold_cons_left]

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