fold_insert_idem — Mathlib

English

If op is idempotent, folding over insert a s reduces to the standard insert case with a simplified equality when a ∈ s or a ∉ s.

Русский

Если операция идемпотентна, свёртка по insert a s упрощается до стандартного случая вставки, со специальными преобразованиями.

LaTeX

$$$(\\mathrm{insert}\\ a\\ s).fold op b f = op (f a) (s.fold op b f)$$$

Lean4

@[simp]
theorem fold_insert_idem [DecidableEq α] [hi : Std.IdempotentOp op] : (insert a s).fold op b f = f a * s.fold op b f :=
  by
  by_cases h : a ∈ s
  · rw [← insert_erase h]
    simp [← ha.assoc, hi.idempotent]
  · apply fold_insert h

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