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] :
fold op b s folds a commutative associative operation op over
the multiset s.
Equations
- multiset.fold op = multiset.foldr op _
theorem
multiset.fold_eq_foldr
{α : Type u_1}
(op : α → α → α)
[hc : is_commutative α op]
[ha : is_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 : is_commutative α op]
[ha : is_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 : is_commutative α op]
[ha : is_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 : is_commutative α op]
[ha : is_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 : 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 : α) :
multiset.fold op b s.dedup = multiset.fold op b s
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.max_nat_le_of_forall_le
(l : multiset ℕ)
(n : ℕ)
(h : ∀ (x : ℕ), x ∈ l → x ≤ n) :
multiset.fold linear_order.max 0 l ≤ n