fold_insert — Mathlib

English

If a ∉ s and a is decidable, then fold op b f (insert a s) = op(f a, fold op b f s).

Русский

Если a не в s, то fold op b f (insert a s) = op(f a, fold op b f s).

LaTeX

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

Lean4

@[simp]
theorem fold_insert [DecidableEq α] (h : a ∉ s) : (insert a s).fold op b f = f a * s.fold op b f :=
  by
  unfold fold
  rw [insert_val, ndinsert_of_notMem h, Multiset.map_cons, fold_cons_left]

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