The fold operation for a commutative associative operation over a multiset. #
fold #
def
Multiset.fold
{α : Type u_1}
(op : α → α → α)
[hc : Std.Commutative op]
[ha : Std.Associative op]
:
α → Multiset α → α
fold op b s folds a commutative associative operation op over
the multiset s.
Equations
- Multiset.fold op = Multiset.foldr op
Instances For
theorem
Multiset.fold_eq_foldr
{α : Type u_1}
(op : α → α → α)
[hc : Std.Commutative op]
[ha : Std.Associative op]
(b : α)
(s : Multiset α)
:
Multiset.fold op b s = Multiset.foldr op b s
@[simp]
theorem
Multiset.coe_fold_r
{α : Type u_1}
(op : α → α → α)
[hc : Std.Commutative op]
[ha : Std.Associative op]
(b : α)
(l : List α)
:
Multiset.fold op b ↑l = List.foldr op b l
theorem
Multiset.coe_fold_l
{α : Type u_1}
(op : α → α → α)
[hc : Std.Commutative op]
[ha : Std.Associative op]
(b : α)
(l : List α)
:
Multiset.fold op b ↑l = List.foldl op b l
theorem
Multiset.fold_eq_foldl
{α : Type u_1}
(op : α → α → α)
[hc : Std.Commutative op]
[ha : Std.Associative op]
(b : α)
(s : Multiset α)
:
Multiset.fold op b s = Multiset.foldl op b s
@[simp]
theorem
Multiset.fold_zero
{α : Type u_1}
(op : α → α → α)
[hc : Std.Commutative op]
[ha : Std.Associative op]
(b : α)
:
Multiset.fold op b 0 = b
@[simp]
theorem
Multiset.fold_cons_left
{α : Type u_1}
(op : α → α → α)
[hc : Std.Commutative op]
[ha : Std.Associative op]
(b a : α)
(s : Multiset α)
:
Multiset.fold op b (a ::ₘ s) = op a (Multiset.fold op b s)
theorem
Multiset.fold_cons_right
{α : Type u_1}
(op : α → α → α)
[hc : Std.Commutative op]
[ha : Std.Associative op]
(b a : α)
(s : Multiset α)
:
Multiset.fold op b (a ::ₘ s) = op (Multiset.fold op b s) a
theorem
Multiset.fold_cons'_right
{α : Type u_1}
(op : α → α → α)
[hc : Std.Commutative op]
[ha : Std.Associative op]
(b a : α)
(s : Multiset α)
:
Multiset.fold op b (a ::ₘ s) = Multiset.fold op (op b a) s
theorem
Multiset.fold_cons'_left
{α : Type u_1}
(op : α → α → α)
[hc : Std.Commutative op]
[ha : Std.Associative op]
(b a : α)
(s : Multiset α)
:
Multiset.fold op b (a ::ₘ s) = Multiset.fold op (op a b) s
theorem
Multiset.fold_add
{α : Type u_1}
(op : α → α → α)
[hc : Std.Commutative op]
[ha : Std.Associative op]
(b₁ b₂ : α)
(s₁ s₂ : Multiset α)
:
Multiset.fold op (op b₁ b₂) (s₁ + s₂) = op (Multiset.fold op b₁ s₁) (Multiset.fold op b₂ s₂)
theorem
Multiset.fold_bind
{α : Type u_1}
(op : α → α → α)
[hc : Std.Commutative op]
[ha : Std.Associative op]
{ι : Type u_3}
(s : Multiset ι)
(t : ι → Multiset α)
(b : ι → α)
(b₀ : α)
:
Multiset.fold op (Multiset.fold op b₀ (Multiset.map b s)) (s.bind t) = Multiset.fold op b₀ (Multiset.map (fun (i : ι) => Multiset.fold op (b i) (t i)) s)
theorem
Multiset.fold_singleton
{α : Type u_1}
(op : α → α → α)
[hc : Std.Commutative op]
[ha : Std.Associative op]
(b a : α)
:
Multiset.fold op b {a} = op a b
theorem
Multiset.fold_distrib
{α : Type u_1}
{β : Type u_2}
(op : α → α → α)
[hc : Std.Commutative op]
[ha : Std.Associative op]
{f g : β → α}
(u₁ u₂ : α)
(s : Multiset β)
:
Multiset.fold op (op u₁ u₂) (Multiset.map (fun (x : β) => op (f x) (g x)) s) = op (Multiset.fold op u₁ (Multiset.map f s)) (Multiset.fold op u₂ (Multiset.map g s))
theorem
Multiset.fold_hom
{α : Type u_1}
{β : Type u_2}
(op : α → α → α)
[hc : Std.Commutative op]
[ha : Std.Associative op]
{op' : β → β → β}
[Std.Commutative op']
[Std.Associative op']
{m : α → β}
(hm : ∀ (x y : α), m (op x y) = op' (m x) (m y))
(b : α)
(s : Multiset α)
:
Multiset.fold op' (m b) (Multiset.map m s) = m (Multiset.fold op b s)
theorem
Multiset.fold_union_inter
{α : Type u_1}
(op : α → α → α)
[hc : Std.Commutative op]
[ha : Std.Associative op]
[DecidableEq α]
(s₁ s₂ : Multiset α)
(b₁ b₂ : α)
:
op (Multiset.fold op b₁ (s₁ ∪ s₂)) (Multiset.fold op b₂ (s₁ ∩ s₂)) = op (Multiset.fold op b₁ s₁) (Multiset.fold op b₂ s₂)
@[simp]
theorem
Multiset.fold_dedup_idem
{α : Type u_1}
(op : α → α → α)
[hc : Std.Commutative op]
[ha : Std.Associative op]
[DecidableEq α]
[hi : Std.IdempotentOp op]
(s : Multiset α)
(b : α)
:
Multiset.fold op b s.dedup = Multiset.fold op b s