Big operators on a multiset in ordered groups #
This file contains the results concerning the interaction of multiset big operators with ordered groups.
theorem
Multiset.le_prod_of_submultiplicative_on_pred
{α : Type u_2}
{β : Type u_3}
[CommMonoid α]
[OrderedCommMonoid β]
(f : α → β)
(p : α → Prop)
(h_one : f 1 = 1)
(hp_one : p 1)
(h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b)
(hp_mul : ∀ (a b : α), p a → p b → p (a * b))
(s : Multiset α)
(hps : ∀ a ∈ s, p a)
:
theorem
Multiset.le_sum_of_subadditive_on_pred
{α : Type u_2}
{β : Type u_3}
[AddCommMonoid α]
[OrderedAddCommMonoid β]
(f : α → β)
(p : α → Prop)
(h_one : f 0 = 0)
(hp_one : p 0)
(h_mul : ∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b)
(hp_mul : ∀ (a b : α), p a → p b → p (a + b))
(s : Multiset α)
(hps : ∀ a ∈ s, p a)
:
theorem
Multiset.le_prod_nonempty_of_submultiplicative_on_pred
{α : Type u_2}
{β : Type u_3}
[CommMonoid α]
[OrderedCommMonoid β]
(f : α → β)
(p : α → Prop)
(h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b)
(hp_mul : ∀ (a b : α), p a → p b → p (a * b))
(s : Multiset α)
(hs_nonempty : s ≠ ∅)
(hs : ∀ a ∈ s, p a)
:
theorem
Multiset.le_sum_nonempty_of_subadditive_on_pred
{α : Type u_2}
{β : Type u_3}
[AddCommMonoid α]
[OrderedAddCommMonoid β]
(f : α → β)
(p : α → Prop)
(h_mul : ∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b)
(hp_mul : ∀ (a b : α), p a → p b → p (a + b))
(s : Multiset α)
(hs_nonempty : s ≠ ∅)
(hs : ∀ a ∈ s, p a)
:
theorem
Multiset.prod_eq_one_iff
{α : Type u_2}
[OrderedCommMonoid α]
[CanonicallyOrderedMul α]
{m : Multiset α}
:
theorem
Multiset.sum_eq_zero_iff
{α : Type u_2}
[OrderedAddCommMonoid α]
[CanonicallyOrderedAdd α]
{m : Multiset α}
:
theorem
Multiset.le_prod_of_mem
{α : Type u_2}
[OrderedCommMonoid α]
[CanonicallyOrderedMul α]
{m : Multiset α}
{a : α}
(ha : a ∈ m)
:
theorem
Multiset.le_sum_of_mem
{α : Type u_2}
[OrderedAddCommMonoid α]
[CanonicallyOrderedAdd α]
{m : Multiset α}
{a : α}
(ha : a ∈ m)
: