The fold operation for a commutative associative operation over a multiset.

fold

def Multiset.fold {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] : α → Multiset α → α

fold op b s folds a commutative associative operation op over the multiset s.

Equations

• Multiset.fold op = Multiset.foldr op (_ : LeftCommutative op)

theorem Multiset.fold_eq_foldr {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (s : Multiset α) : Multiset.fold op b s = Multiset.foldr op (_ : LeftCommutative op) b s

@[simp]

theorem Multiset.coe_fold_r {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (l : List α) : Multiset.fold op b ↑l = List.foldr op b l

theorem Multiset.coe_fold_l {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (l : List α) : Multiset.fold op b ↑l = List.foldl op b l

theorem Multiset.fold_eq_foldl {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) (s : Multiset α) : Multiset.fold op b s = Multiset.foldl op (_ : RightCommutative op) b s

@[simp]

theorem Multiset.fold_zero {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α op] (b : α) : Multiset.fold op b 0 = b

@[simp]

theorem Multiset.fold_cons_left {α : Type u_1} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α 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 : IsCommutative α op] [ha : IsAssociative α 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 : IsCommutative α op] [ha : IsAssociative α 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 : IsCommutative α op] [ha : IsAssociative α 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 : IsCommutative α op] [ha : IsAssociative α op] (b₁ : α) (b₂ : α) (s₁ : Multiset α) (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 : IsCommutative α op] [ha : IsAssociative α op] {ι : Type u_3} (s : Multiset ι) (t : ι → Multiset α) (b : ι → α) (b₀ : α) : Multiset.fold op (Multiset.fold op b₀ (Multiset.map b s)) (Multiset.bind s 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 : IsCommutative α op] [ha : IsAssociative α op] (b : α) (a : α) : Multiset.fold op b {a} = op a b

theorem Multiset.fold_distrib {α : Type u_1} {β : Type u_2} (op : α → α → α) [hc : IsCommutative α op] [ha : IsAssociative α 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 : IsCommutative α op] [ha : IsAssociative α op] {op' : β → β → β} [IsCommutative β op'] [IsAssociative β 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 : IsCommutative α op] [ha : IsAssociative α op] [DecidableEq α] (s₁ : Multiset α) (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 : IsCommutative α op] [ha : IsAssociative α op] [DecidableEq α] [hi : IsIdempotent α op] (s : Multiset α) (b : α) : Multiset.fold op b (Multiset.dedup s) = Multiset.fold op b s

theorem Multiset.max_le_of_forall_le {α : Type u_3} [CanonicallyLinearOrderedAddCommMonoid α] (l : Multiset α) (n : α) (h : ∀ x ∈ l, x ≤ n) : Multiset.fold max ⊥ l ≤ n

theorem Multiset.max_nat_le_of_forall_le (l : Multiset ℕ) (n : ℕ) (h : ∀ x ∈ l, x ≤ n) : Multiset.fold max 0 l ≤ n

theorem Multiset.le_smul_dedup {α : Type u_1} [DecidableEq α] (s : Multiset α) : ∃ (n : ℕ), s ≤ n • Multiset.dedup s