mathlib3 documentation

data.multiset.fold

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

fold #

def multiset.fold {α : Type u_1} (op : α α α) [hc : is_commutative α op] [ha : is_associative α op] :
α multiset α α

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

Equations
theorem multiset.fold_eq_foldr {α : Type u_1} (op : α α α) [hc : is_commutative α op] [ha : is_associative α op] (b : α) (s : multiset α) :
@[simp]
theorem multiset.coe_fold_r {α : Type u_1} (op : α α α) [hc : is_commutative α op] [ha : is_associative α op] (b : α) (l : list α) :
theorem multiset.coe_fold_l {α : Type u_1} (op : α α α) [hc : is_commutative α op] [ha : is_associative α op] (b : α) (l : list α) :
theorem multiset.fold_eq_foldl {α : Type u_1} (op : α α α) [hc : is_commutative α op] [ha : is_associative α op] (b : α) (s : multiset α) :
@[simp]
theorem multiset.fold_zero {α : Type u_1} (op : α α α) [hc : is_commutative α op] [ha : is_associative α op] (b : α) :
multiset.fold op b 0 = b
@[simp]
theorem multiset.fold_cons_left {α : Type u_1} (op : α α α) [hc : is_commutative α op] [ha : is_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 : is_commutative α op] [ha : is_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 : is_commutative α op] [ha : is_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 : is_commutative α op] [ha : is_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 : is_commutative α op] [ha : is_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 : is_commutative α op] [ha : is_associative α op] {ι : Type u_2} (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 (λ (i : ι), multiset.fold op (b i) (t i)) s)
theorem multiset.fold_singleton {α : Type u_1} (op : α α α) [hc : is_commutative α op] [ha : is_associative α op] (b a : α) :
multiset.fold op b {a} = op a b
theorem multiset.fold_distrib {α : Type u_1} {β : Type u_2} (op : α α α) [hc : is_commutative α op] [ha : is_associative α op] {f g : β α} (u₁ u₂ : α) (s : multiset β) :
multiset.fold op (op u₁ u₂) (multiset.map (λ (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 : is_commutative α op] [ha : is_associative α op] {op' : β β β} [is_commutative β op'] [is_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 : is_commutative α op] [ha : is_associative α op] [decidable_eq α] (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 : is_commutative α op] [ha : is_associative α op] [decidable_eq α] [hi : is_idempotent α op] (s : multiset α) (b : α) :
theorem multiset.max_le_of_forall_le {α : Type u_1} [canonically_linear_ordered_add_monoid α] (l : multiset α) (n : α) (h : (x : α), x l x n) :
theorem multiset.le_smul_dedup {α : Type u_1} [decidable_eq α] (s : multiset α) :
(n : ), s n s.dedup