Multiset.le_sum_of_mem
theorem Multiset.le_sum_of_mem :
∀ {α : Type u_2} [inst : CanonicallyOrderedAddCommMonoid α] {m : Multiset α} {a : α}, a ∈ m → a ≤ m.sum
This theorem states that for any type `α` which has a `CanonicallyOrderedAddCommMonoid` structure, and for any multiset `s` of type `α` and any element `a` of type `α`, if `a` is an element of `s`, then `a` is less than or equal to the sum of all the elements of `s`. This is true because in a `CanonicallyOrderedAddCommMonoid`, the sum operation is commutative, associative and has an identity element, and the order is compatible with the addition operation, i.e., if `b ≤ c` then `a + b ≤ a + c`.
More concisely: For any `CanonicallyOrderedAddCommMonoid` type `α` and multiset `s` of `α`, if `a` is in `s`, then `a ≤ sum s`.
|
Multiset.le_sum_of_subadditive
theorem Multiset.le_sum_of_subadditive :
∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : OrderedAddCommMonoid β] (f : α → β),
f 0 = 0 → (∀ (a b : α), f (a + b) ≤ f a + f b) → ∀ (s : Multiset α), f s.sum ≤ (Multiset.map f s).sum
This theorem, `Multiset.le_sum_of_subadditive`, states that for any types `α` and `β` where `α` is a commutative additive monoid and `β` is an ordered commutative additive monoid, and given a function `f` from `α` to `β` with the properties: (1) `f` of 0 is 0, and (2) for any `a` and `b` from `α`, `f` of `a + b` is less than or equal to `f` of `a` plus `f` of `b` (i.e., `f` is subadditive), then for any multiset `s` of type `α`, `f` of the sum of `s` is less than or equal to the sum of the multiset obtained by applying `f` to each element of `s`.
In mathematical terms, it says that for a function `f : α → β` that is subadditive (meaning `f(a + b) ≤ f(a) + f(b)`), the value of `f` on the sum of a multiset is less than or equal to the sum of the values of `f` on each element of the multiset.
More concisely: For any subadditive function `f : α → β` where `α` is a commutative additive monoid and `β` is an ordered commutative additive monoid, the application of `f` to the sum of a multiset `s` in `α` is less than or equal to the sum of the applications of `f` to each element in `s`.
|