Multiset.fold_add
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₂)
The theorem `Multiset.fold_add` states that for any type `α`, any binary operation `op` on `α` that is both commutative and associative, any two elements `b₁` and `b₂` of `α`, and any two multisets `s₁` and `s₂` of elements of `α`, the result of folding `op` over the combination of `s₁` and `s₂` starting from `op b₁ b₂` is the same as applying `op` to the result of folding `op` over `s₁` starting from `b₁` and the result of folding `op` over `s₂` starting from `b₂`. In mathematical terms, this states that for all such `op`, `b₁`, `b₂`, `s₁`, `s₂`, we have `Multiset.fold op (op b₁ b₂) (s₁ + s₂) = op (Multiset.fold op b₁ s₁) (Multiset.fold op b₂ s₂)`. This is essentially a distributive property of the `Multiset.fold` operation over multiset addition.
More concisely: For any commutative and associative binary operation `op` on type `α`, and multisets `s₁` and `s₂` of `α`, we have `Multiset.fold op (op (b₁ :: s₁) b₂ :: s₂) = op (Multiset.fold op b₁ s₁) (Multiset.fold op b₂ s₂)`, where `b₁` and `b₂` are elements of `α`.
|
Multiset.fold_zero
theorem Multiset.fold_zero :
∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b : α),
Multiset.fold op b 0 = b
The theorem `Multiset.fold_zero` states that for any type `α`, any binary operation `op` that is both commutative and associative, and any value `b` of type `α`, the result of folding the operation `op` over an empty multiset (represented as `0`) starting with `b` is `b`. In other words, applying a commutative and associative operation iteratively over no elements leaves the initial value unchanged.
More concisely: For any commutative and associative binary operation `op` and value `b`, the empty multiset fold of `op` starting with `b` equals `b`. In other words, `Multiset.fold op b Ø = b`.
|
Multiset.fold_dedup_idem
theorem Multiset.fold_dedup_idem :
∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] [inst : DecidableEq α]
[hi : Std.IdempotentOp op] (s : Multiset α) (b : α), Multiset.fold op b s.dedup = Multiset.fold op b s
The theorem `Multiset.fold_dedup_idem` states that for any type `α` with a decidable equality, a binary operation `op` that is commutative, associative, and idempotent, a multiset `s` of type `α`, and an element `b` of type `α`, the result of folding `op` over the deduplicated multiset `s` with initial element `b` is the same as folding `op` over `s` with initial element `b`. In simpler terms, it means that if we remove duplicates from the multiset before folding, the result is the same as if we didn't remove duplicates, as long as the operation `op` is idempotent (applying `op` twice or more times to the same elements gives the same result as applying it once).
More concisely: For any commutative, associative, and idempotent binary operation `op` on type `α` with decidable equality, and any multiset `s` of type `α` and element `b` of type `α`, the result of folding `op` over the deduplicated multiset `s` with initial element `b` is equal to folding `op` over `s` with initial element `b`.
|
Multiset.fold.proof_1
theorem Multiset.fold.proof_1 :
∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op], LeftCommutative op := by
sorry
This theorem states that for all types `α`, given a binary operation `op` on `α`, if `op` is both commutative and associative, then `op` is also left commutative. In other words, for any two elements `a₁` and `a₂` of type `α` and any element `b` of the same type, the result of applying `op` on `a₁` and the result of applying `op` on `a₂` and `b` is the same as applying `op` on `a₂` and the result of applying `op` on `a₁` and `b`. This is expressed in Lean 4 by `h a₁ (h a₂ b) = h a₂ (h a₁ b)` where `h` is `op`.
More concisely: If a binary operation `op` on type `α` is commutative and associative, then it is left commutative, i.e., `a₁ op a₂ = a₂ op a₁` for all `a₁, a₂ : α`.
|
Multiset.fold_cons_left
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)
The theorem `Multiset.fold_cons_left` states that for any given type `α`, an operation `op` that is both commutative and associative, elements `b` and `a` of type `α`, and a multiset `s` of type `α`, applying the `fold` function with operation `op` and element `b` to the multiset obtained by adding `a` to `s` is equivalent to applying the operation `op` on `a` and the result of applying the `fold` function with operation `op` and element `b` to multiset `s`.
More concisely: For any commutative and associative operation `op` on type `α`, and multisets `s` and `t` such that `t = s ++ {a}`, the result of `fold op b (s ++ {a})` is equal to `op a (fold op b s)`.
|