# Big operators on a finset in ordered groups #

This file contains the results concerning the interaction of multiset big operators with ordered groups/monoids.

source
theorem Finset.le_prod_nonempty_of_submultiplicative_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [CommMonoid M] [CommMonoid N] [PartialOrder N] [IsOrderedMonoid N] (f : M → N) (p : M → Prop) (h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) (hp_mul : ∀ (x y : M), p x → p y → p (x * y)) (g : ι → M) (s : Finset ι) (hs_nonempty : s.Nonempty) (hs : ∀ i ∈ s, p (g i)) :
f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Let `{x | p x}` be a subsemigroup of a commutative monoid `M`. Let `f : M → N` be a map submultiplicative on `{x | p x}`, i.e., `p x → p y → f (x * y) ≤ f x * f y`. Let `g i`, `i ∈ s`, be a nonempty finite family of elements of `M` such that `∀ i ∈ s, p (g i)`. Then `f (∏ x ∈ s, g x) ≤ ∏ x ∈ s, f (g x)`.

source
theorem Finset.le_sum_nonempty_of_subadditive_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [PartialOrder N] [IsOrderedAddMonoid N] (f : M → N) (p : M → Prop) (h_add : ∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) (hp_add : ∀ (x y : M), p x → p y → p (x + y)) (g : ι → M) (s : Finset ι) (hs_nonempty : s.Nonempty) (hs : ∀ i ∈ s, p (g i)) :
f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)

Let `{x | p x}` be an additive subsemigroup of an additive commutative monoid `M`. Let `f : M → N` be a map subadditive on `{x | p x}`, i.e., `p x → p y → f (x + y) ≤ f x + f y`. Let `g i`, `i ∈ s`, be a nonempty finite family of elements of `M` such that `∀ i ∈ s, p (g i)`. Then `f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)`.

source
theorem Finset.le_prod_nonempty_of_submultiplicative {ι : Type u_1} {M : Type u_4} {N : Type u_5} [CommMonoid M] [CommMonoid N] [PartialOrder N] [IsOrderedMonoid N] (f : M → N) (h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y) {s : Finset ι} (hs : s.Nonempty) (g : ι → M) :
f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

If `f : M → N` is a submultiplicative function, `f (x * y) ≤ f x * f y` and `g i`, `i ∈ s`, is a nonempty finite family of elements of `M`, then `f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)`.

source
theorem Finset.le_sum_nonempty_of_subadditive {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [PartialOrder N] [IsOrderedAddMonoid N] (f : M → N) (h_add : ∀ (x y : M), f (x + y) ≤ f x + f y) {s : Finset ι} (hs : s.Nonempty) (g : ι → M) :
f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)

If `f : M → N` is a subadditive function, `f (x + y) ≤ f x + f y` and `g i`, `i ∈ s`, is a nonempty finite family of elements of `M`, then `f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)`.

source
theorem Finset.le_prod_of_submultiplicative_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [CommMonoid M] [CommMonoid N] [PartialOrder N] [IsOrderedMonoid N] (f : M → N) (p : M → Prop) (h_one : f 1 ≤ 1) (h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) (hp_mul : ∀ (x y : M), p x → p y → p (x * y)) (g : ι → M) {s : Finset ι} (hs : ∀ i ∈ s, p (g i)) :
f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Let `{x | p x}` be a subsemigroup of a commutative monoid `M`. Let `f : M → N` be a map such that `f 1 = 1` and `f` is submultiplicative on `{x | p x}`, i.e., `p x → p y → f (x * y) ≤ f x * f y`. Let `g i`, `i ∈ s`, be a finite family of elements of `M` such that `∀ i ∈ s, p (g i)`. Then `f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)`.

source
theorem Finset.le_sum_of_subadditive_on_pred {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [PartialOrder N] [IsOrderedAddMonoid N] (f : M → N) (p : M → Prop) (h_zero : f 0 ≤ 0) (h_add : ∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) (hp_add : ∀ (x y : M), p x → p y → p (x + y)) (g : ι → M) {s : Finset ι} (hs : ∀ i ∈ s, p (g i)) :
f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)

Let `{x | p x}` be a subsemigroup of a commutative additive monoid `M`. Let `f : M → N` be a map such that `f 0 = 0` and `f` is subadditive on `{x | p x}`, i.e. `p x → p y → f (x + y) ≤ f x + f y`. Let `g i`, `i ∈ s`, be a finite family of elements of `M` such that `∀ i ∈ s, p (g i)`. Then `f (∑ x ∈ s, g x) ≤ ∑ x ∈ s, f (g x)`.

source
theorem Finset.le_prod_of_submultiplicative {ι : Type u_1} {M : Type u_4} {N : Type u_5} [CommMonoid M] [CommMonoid N] [PartialOrder N] [IsOrderedMonoid N] (f : M → N) (h_one : f 1 ≤ 1) (h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y) (s : Finset ι) (g : ι → M) :
f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

If `f : M → N` is a submultiplicative function, `f (x * y) ≤ f x * f y`, `f 1 = 1`, and `g i`, `i ∈ s`, is a finite family of elements of `M`, then `f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)`.

source
theorem Finset.le_sum_of_subadditive {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [PartialOrder N] [IsOrderedAddMonoid N] (f : M → N) (h_zero : f 0 ≤ 0) (h_add : ∀ (x y : M), f (x + y) ≤ f x + f y) (s : Finset ι) (g : ι → M) :
f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)

If `f : M → N` is a subadditive function, `f (x + y) ≤ f x + f y`, `f 0 = 0`, and `g i`, `i ∈ s`, is a finite family of elements of `M`, then `f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)`.

source
theorem Finset.prod_le_prod' {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] {f g : ι → N} {s : Finset ι} [MulLeftMono N] (h : ∀ i ∈ s, f i ≤ g i) :
∏ i ∈ s, f i ≤ ∏ i ∈ s, g i

In an ordered commutative monoid, if each factor `f i` of one finite product is less than or equal to the corresponding factor `g i` of another finite product, then `∏ i ∈ s, f i ≤ ∏ i ∈ s, g i`.

source
theorem Finset.sum_le_sum {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {f g : ι → N} {s : Finset ι} [AddLeftMono N] (h : ∀ i ∈ s, f i ≤ g i) :
∑ i ∈ s, f i ≤ ∑ i ∈ s, g i

In an ordered additive commutative monoid, if each summand `f i` of one finite sum is less than or equal to the corresponding summand `g i` of another finite sum, then `∑ i ∈ s, f i ≤ ∑ i ∈ s, g i`.

source
theorem Finset.one_le_prod' {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [MulLeftMono N] (h : ∀ i ∈ s, 1 ≤ f i) :
1 ≤ ∏ i ∈ s, f i
source
theorem Finset.sum_nonneg {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [AddLeftMono N] (h : ∀ i ∈ s, 0 ≤ f i) :
0 ≤ ∑ i ∈ s, f i
source
theorem Finset.one_le_prod'' {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [MulLeftMono N] (h : ∀ (i : ι), 1 ≤ f i) :
1 ≤ ∏ i ∈ s, f i
source
theorem Finset.sum_nonneg' {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [AddLeftMono N] (h : ∀ (i : ι), 0 ≤ f i) :
0 ≤ ∑ i ∈ s, f i
source
theorem Finset.prod_le_one' {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [MulLeftMono N] (h : ∀ i ∈ s, f i ≤ 1) :
∏ i ∈ s, f i ≤ 1
source
theorem Finset.sum_nonpos {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [AddLeftMono N] (h : ∀ i ∈ s, f i ≤ 0) :
∑ i ∈ s, f i ≤ 0
source
theorem Finset.prod_le_prod_of_subset_of_one_le' {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] {f : ι → N} {s t : Finset ι} [MulLeftMono N] (h : s ⊆ t) (hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i) :
∏ i ∈ s, f i ≤ ∏ i ∈ t, f i
source
theorem Finset.sum_le_sum_of_subset_of_nonneg {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {f : ι → N} {s t : Finset ι} [AddLeftMono N] (h : s ⊆ t) (hf : ∀ i ∈ t, i ∉ s → 0 ≤ f i) :
∑ i ∈ s, f i ≤ ∑ i ∈ t, f i
source
theorem Finset.prod_mono_set_of_one_le' {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] {f : ι → N} [MulLeftMono N] (hf : ∀ (x : ι), 1 ≤ f x) :
Monotone fun (s : Finset ι) => ∏ x ∈ s, f x
source
theorem Finset.sum_mono_set_of_nonneg {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {f : ι → N} [AddLeftMono N] (hf : ∀ (x : ι), 0 ≤ f x) :
Monotone fun (s : Finset ι) => ∑ x ∈ s, f x
source
theorem Finset.prod_le_univ_prod_of_one_le' {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] {f : ι → N} [MulLeftMono N] [Fintype ι] {s : Finset ι} (w : ∀ (x : ι), 1 ≤ f x) :
∏ x ∈ s, f x ≤ ∏ x : ι, f x
source
theorem Finset.sum_le_univ_sum_of_nonneg {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {f : ι → N} [AddLeftMono N] [Fintype ι] {s : Finset ι} (w : ∀ (x : ι), 0 ≤ f x) :
∑ x ∈ s, f x ≤ ∑ x : ι, f x
source
theorem Finset.prod_eq_one_iff_of_one_le' {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [MulLeftMono N] :
(∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
source
theorem Finset.sum_eq_zero_iff_of_nonneg {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [AddLeftMono N] :
(∀ i ∈ s, 0 ≤ f i) → (∑ i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0)
source
theorem Finset.one_lt_prod_iff_of_one_le {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [MulLeftMono N] (hf : ∀ x ∈ s, 1 ≤ f x) :
1 < ∏ x ∈ s, f x ↔ ∃ x ∈ s, 1 < f x
source
theorem Finset.sum_pos_iff_of_nonneg {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [AddLeftMono N] (hf : ∀ x ∈ s, 0 ≤ f x) :
0 < ∑ x ∈ s, f x ↔ ∃ x ∈ s, 0 < f x
source
theorem Finset.prod_eq_one_iff_of_le_one' {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [MulLeftMono N] :
(∀ i ∈ s, f i ≤ 1) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
source
theorem Finset.sum_eq_zero_iff_of_nonpos {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [AddLeftMono N] :
(∀ i ∈ s, f i ≤ 0) → (∑ i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0)
source
theorem Finset.prod_lt_one_iff_of_le_one {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [MulLeftMono N] (hf : ∀ x ∈ s, f x ≤ 1) :
∏ x ∈ s, f x < 1 ↔ ∃ x ∈ s, f x < 1
source
theorem Finset.sum_neg_iff_of_nonpos {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [AddLeftMono N] (hf : ∀ x ∈ s, f x ≤ 0) :
∑ x ∈ s, f x < 0 ↔ ∃ x ∈ s, f x < 0
source
theorem Finset.single_le_prod' {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [MulLeftMono N] (hf : ∀ i ∈ s, 1 ≤ f i) {a : ι} (h : a ∈ s) :
f a ≤ ∏ x ∈ s, f x
source
theorem Finset.single_le_sum {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [AddLeftMono N] (hf : ∀ i ∈ s, 0 ≤ f i) {a : ι} (h : a ∈ s) :
f a ≤ ∑ x ∈ s, f x
source
theorem Finset.mul_le_prod {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [MulLeftMono N] {i j : ι} (hf : ∀ i ∈ s, 1 ≤ f i) (hi : i ∈ s) (hj : j ∈ s) (hne : i ≠ j) :
f i * f j ≤ ∏ k ∈ s, f k
source
theorem Finset.add_le_sum {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {f : ι → N} {s : Finset ι} [AddLeftMono N] {i j : ι} (hf : ∀ i ∈ s, 0 ≤ f i) (hi : i ∈ s) (hj : j ∈ s) (hne : i ≠ j) :
f i + f j ≤ ∑ k ∈ s, f k
source
theorem Finset.prod_le_pow_card {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] [MulLeftMono N] (s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, f x ≤ n) :
s.prod f ≤ n ^ s.card
source
theorem Finset.sum_le_card_nsmul {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] [AddLeftMono N] (s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, f x ≤ n) :
s.sum f ≤ s.card • n
source
theorem Finset.pow_card_le_prod {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] [MulLeftMono N] (s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, n ≤ f x) :
n ^ s.card ≤ s.prod f
source
theorem Finset.card_nsmul_le_sum {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] [AddLeftMono N] (s : Finset ι) (f : ι → N) (n : N) (h : ∀ x ∈ s, n ≤ f x) :
s.card • n ≤ s.sum f
source
theorem Finset.card_biUnion_le_card_mul {ι : Type u_1} {β : Type u_3} [DecidableEq β] (s : Finset ι) (f : ι → Finset β) (n : ℕ) (h : ∀ a ∈ s, (f a).card ≤ n) :
(s.biUnion f).card ≤ s.card * n
source
theorem Finset.prod_fiberwise_le_prod_of_one_le_prod_fiber' {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] [MulLeftMono N] {t : Finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ y ∉ t, 1 ≤ ∏ x ∈ s with g x = y, f x) :
∏ y ∈ t, ∏ x ∈ s with g x = y, f x ≤ ∏ x ∈ s, f x
source
theorem Finset.sum_fiberwise_le_sum_of_sum_fiber_nonneg {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] [AddLeftMono N] {t : Finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ y ∉ t, 0 ≤ ∑ x ∈ s with g x = y, f x) :
∑ y ∈ t, ∑ x ∈ s with g x = y, f x ≤ ∑ x ∈ s, f x
source
theorem Finset.prod_le_prod_fiberwise_of_prod_fiber_le_one' {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] [MulLeftMono N] {t : Finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ y ∉ t, ∏ x ∈ s with g x = y, f x ≤ 1) :
∏ x ∈ s, f x ≤ ∏ y ∈ t, ∏ x ∈ s with g x = y, f x
source
theorem Finset.sum_le_sum_fiberwise_of_sum_fiber_nonpos {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] [AddLeftMono N] {t : Finset ι'} {g : ι → ι'} {f : ι → N} (h : ∀ y ∉ t, ∑ x ∈ s with g x = y, f x ≤ 0) :
∑ x ∈ s, f x ≤ ∑ y ∈ t, ∑ x ∈ s with g x = y, f x
source
theorem Finset.prod_image_le_of_one_le {ι : Type u_1} {N : Type u_5} [CommMonoid N] [PartialOrder N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] [MulLeftMono N] {g : ι → ι'} {f : ι' → N} (hf : ∀ u ∈ image g s, 1 ≤ f u) :
∏ u ∈ image g s, f u ≤ ∏ u ∈ s, f (g u)
source
theorem Finset.sum_image_le_of_nonneg {ι : Type u_1} {N : Type u_5} [AddCommMonoid N] [PartialOrder N] {s : Finset ι} {ι' : Type u_9} [DecidableEq ι'] [AddLeftMono N] {g : ι → ι'} {f : ι' → N} (hf : ∀ u ∈ image g s, 0 ≤ f u) :
∑ u ∈ image g s, f u ≤ ∑ u ∈ s, f (g u)
source
theorem Finset.apply_prod_le_sum_apply {ι : Type u_1} {α : Type u_2} {β : Type u_3} [CommMonoid α] [AddCommMonoid β] [Preorder β] [AddLeftMono β] (s : Finset ι) {f : ι → α} (g : α → β) (h_one : g 1 ≤ 0) (h_mul : ∀ (a b : α), g (a * b) ≤ g a + g b) :
g (∏ x ∈ s, f x) ≤ ∑ x ∈ s, g (f x)
source
theorem Finset.sum_apply_le_apply_prod {ι : Type u_1} {α : Type u_2} {β : Type u_3} [CommMonoid α] [AddCommMonoid β] [Preorder β] [AddLeftMono β] (s : Finset ι) {f : ι → α} (g : α → β) (h_one : 0 ≤ g 1) (h_mul : ∀ (a b : α), g a + g b ≤ g (a * b)) :
∑ x ∈ s, g (f x) ≤ g (∏ x ∈ s, f x)
source
theorem Finset.max_prod_le {ι : Type u_1} {M : Type u_4} [CommMonoid M] [LinearOrder M] [IsOrderedMonoid M] {f g : ι → M} {s : Finset ι} :
max (s.prod f) (s.prod g) ≤ ∏ i ∈ s, max (f i) (g i)
source
theorem Finset.max_sum_le {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [LinearOrder M] [IsOrderedAddMonoid M] {f g : ι → M} {s : Finset ι} :
max (s.sum f) (s.sum g) ≤ ∑ i ∈ s, max (f i) (g i)
source
theorem Finset.prod_min_le {ι : Type u_1} {M : Type u_4} [CommMonoid M] [LinearOrder M] [IsOrderedMonoid M] {f g : ι → M} {s : Finset ι} :
∏ i ∈ s, min (f i) (g i) ≤ min (s.prod f) (s.prod g)
source
theorem Finset.sum_min_le {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [LinearOrder M] [IsOrderedAddMonoid M] {f g : ι → M} {s : Finset ι} :
∑ i ∈ s, min (f i) (g i) ≤ min (s.sum f) (s.sum g)
source
theorem Finset.abs_sum_le_sum_abs {ι : Type u_1} {G : Type u_9} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (f : ι → G) (s : Finset ι) :
|∑ i ∈ s, f i| ≤ ∑ i ∈ s, |f i|
source
theorem Finset.abs_sum_of_nonneg {ι : Type u_1} {G : Type u_9} [AddCommGroup G] [LinearOrder G] [AddLeftMono G] {f : ι → G} {s : Finset ι} (hf : ∀ i ∈ s, 0 ≤ f i) :
|∑ i ∈ s, f i| = ∑ i ∈ s, f i
source
theorem Finset.abs_sum_of_nonneg' {ι : Type u_1} {G : Type u_9} [AddCommGroup G] [LinearOrder G] [AddLeftMono G] {f : ι → G} {s : Finset ι} (hf : ∀ (i : ι), 0 ≤ f i) :
|∑ i ∈ s, f i| = ∑ i ∈ s, f i
source
@[simp]
theorem Finset.mulLECancellable_prod {ι : Type u_1} {α : Type u_2} [CommMonoid α] [LE α] [MulLeftMono α] {s : Finset ι} {f : ι → α} :
MulLECancellable (∏ i ∈ s, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s → MulLECancellable (f i)
source
@[simp]
theorem Finset.addLECancellable_sum {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [LE α] [AddLeftMono α] {s : Finset ι} {f : ι → α} :
AddLECancellable (∑ i ∈ s, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s → AddLECancellable (f i)
source
theorem Finset.card_le_mul_card_image_of_maps_to {α : Type u_2} {β : Type u_3} [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β} (Hf : ∀ a ∈ s, f a ∈ t) (n : ℕ) (hn : ∀ b ∈ t, {a ∈ s | f a = b}.card ≤ n) :
s.card ≤ n * t.card
source
theorem Finset.card_le_mul_card_image {α : Type u_2} {β : Type u_3} [DecidableEq β] {f : α → β} (s : Finset α) (n : ℕ) (hn : ∀ b ∈ image f s, {a ∈ s | f a = b}.card ≤ n) :
s.card ≤ n * (image f s).card
source
theorem Finset.mul_card_image_le_card_of_maps_to {α : Type u_2} {β : Type u_3} [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β} (Hf : ∀ a ∈ s, f a ∈ t) (n : ℕ) (hn : ∀ b ∈ t, n ≤ {a ∈ s | f a = b}.card) :
n * t.card ≤ s.card
source
theorem Finset.mul_card_image_le_card {α : Type u_2} {β : Type u_3} [DecidableEq β] {f : α → β} (s : Finset α) (n : ℕ) (hn : ∀ b ∈ image f s, n ≤ {a ∈ s | f a = b}.card) :
n * (image f s).card ≤ s.card
source
theorem Finset.sum_card_inter_le {α : Type u_2} [DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ} (h : ∀ a ∈ s, {b ∈ B | a ∈ b}.card ≤ n) :
∑ t ∈ B, (s ∩ t).card ≤ s.card * n

If every element belongs to at most `n` Finsets, then the sum of their sizes is at most `n` times how many they are.

source
theorem Finset.sum_card_le {α : Type u_2} [DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [Fintype α] (h : ∀ (a : α), {b ∈ B | a ∈ b}.card ≤ n) :
∑ s ∈ B, s.card ≤ Fintype.card α * n

If every element belongs to at most `n` Finsets, then the sum of their sizes is at most `n` times how many they are.

source
theorem Finset.le_sum_card_inter {α : Type u_2} [DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ} (h : ∀ a ∈ s, n ≤ {b ∈ B | a ∈ b}.card) :
s.card * n ≤ ∑ t ∈ B, (s ∩ t).card

If every element belongs to at least `n` Finsets, then the sum of their sizes is at least `n` times how many they are.

source
theorem Finset.le_sum_card {α : Type u_2} [DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [Fintype α] (h : ∀ (a : α), n ≤ {b ∈ B | a ∈ b}.card) :
Fintype.card α * n ≤ ∑ s ∈ B, s.card

If every element belongs to at least `n` Finsets, then the sum of their sizes is at least `n` times how many they are.

source
theorem Finset.sum_card_inter {α : Type u_2} [DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ} (h : ∀ a ∈ s, {b ∈ B | a ∈ b}.card = n) :
∑ t ∈ B, (s ∩ t).card = s.card * n

If every element belongs to exactly `n` Finsets, then the sum of their sizes is `n` times how many they are.

source
theorem Finset.sum_card {α : Type u_2} [DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [Fintype α] (h : ∀ (a : α), {b ∈ B | a ∈ b}.card = n) :
∑ s ∈ B, s.card = Fintype.card α * n

If every element belongs to exactly `n` Finsets, then the sum of their sizes is `n` times how many they are.

source
theorem Finset.card_le_card_biUnion {ι : Type u_1} {α : Type u_2} [DecidableEq α] {s : Finset ι} {f : ι → Finset α} (hs : (↑s).PairwiseDisjoint f) (hf : ∀ i ∈ s, (f i).Nonempty) :
s.card ≤ (s.biUnion f).card
source
theorem Finset.card_le_card_biUnion_add_card_fiber {ι : Type u_1} {α : Type u_2} [DecidableEq α] {s : Finset ι} {f : ι → Finset α} (hs : (↑s).PairwiseDisjoint f) :
s.card ≤ (s.biUnion f).card + {i ∈ s | f i = ∅}.card
source
theorem Finset.card_le_card_biUnion_add_one {ι : Type u_1} {α : Type u_2} [DecidableEq α] {s : Finset ι} {f : ι → Finset α} (hf : Function.Injective f) (hs : (↑s).PairwiseDisjoint f) :
s.card ≤ (s.biUnion f).card + 1
source
theorem Finset.single_le_prod_of_canonicallyOrdered {ι : Type u_1} {M : Type u_4} [CommMonoid M] [PartialOrder M] [CanonicallyOrderedMul M] {f : ι → M} {s : Finset ι} {i : ι} (hi : i ∈ s) :
f i ≤ ∏ j ∈ s, f j

In a canonically-ordered monoid, a product bounds each of its terms.

See also `Finset.single_le_prod'`.

source
theorem Finset.single_le_sum_of_canonicallyOrdered {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [CanonicallyOrderedAdd M] {f : ι → M} {s : Finset ι} {i : ι} (hi : i ∈ s) :
f i ≤ ∑ j ∈ s, f j

In a canonically-ordered additive monoid, a sum bounds each of its terms.

See also `Finset.single_le_sum`.

source
@[deprecated Finset.single_le_prod_of_canonicallyOrdered (since := "2025-09-06")]
theorem CanonicallyOrderedCommMonoid.single_le_prod {ι : Type u_1} {M : Type u_4} [CommMonoid M] [PartialOrder M] [CanonicallyOrderedMul M] {f : ι → M} {s : Finset ι} {i : ι} (hi : i ∈ s) :
f i ≤ ∏ j ∈ s, f j

Alias of `Finset.single_le_prod_of_canonicallyOrdered`.

In a canonically-ordered monoid, a product bounds each of its terms.

See also `Finset.single_le_prod'`.

source
@[deprecated Finset.single_le_sum_of_canonicallyOrdered (since := "2025-09-06")]
theorem CanonicallyOrderedAddCommMonoid.single_le_sum {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [CanonicallyOrderedAdd M] {f : ι → M} {s : Finset ι} {i : ι} (hi : i ∈ s) :
f i ≤ ∑ j ∈ s, f j

Alias of `Finset.single_le_sum_of_canonicallyOrdered`.

In a canonically-ordered additive monoid, a sum bounds each of its terms.

See also `Finset.single_le_sum`.

source
theorem Finset.prod_le_prod_of_subset' {ι : Type u_1} {M : Type u_4} [CommMonoid M] [PartialOrder M] [CanonicallyOrderedMul M] {f : ι → M} {s t : Finset ι} (h : s ⊆ t) :
∏ x ∈ s, f x ≤ ∏ x ∈ t, f x
source
theorem Finset.sum_le_sum_of_subset {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [CanonicallyOrderedAdd M] {f : ι → M} {s t : Finset ι} (h : s ⊆ t) :
∑ x ∈ s, f x ≤ ∑ x ∈ t, f x
source
theorem Finset.prod_mono_set' {ι : Type u_1} {M : Type u_4} [CommMonoid M] [PartialOrder M] [CanonicallyOrderedMul M] (f : ι → M) :
Monotone fun (s : Finset ι) => ∏ x ∈ s, f x
source
theorem Finset.sum_mono_set {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [CanonicallyOrderedAdd M] (f : ι → M) :
Monotone fun (s : Finset ι) => ∑ x ∈ s, f x
source
theorem Finset.prod_le_prod_of_ne_one' {ι : Type u_1} {M : Type u_4} [CommMonoid M] [PartialOrder M] [CanonicallyOrderedMul M] {f : ι → M} {s t : Finset ι} (h : ∀ x ∈ s, f x ≠ 1 → x ∈ t) :
∏ x ∈ s, f x ≤ ∏ x ∈ t, f x
source
theorem Finset.sum_le_sum_of_ne_zero {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [CanonicallyOrderedAdd M] {f : ι → M} {s t : Finset ι} (h : ∀ x ∈ s, f x ≠ 0 → x ∈ t) :
∑ x ∈ s, f x ≤ ∑ x ∈ t, f x
source
theorem Finset.one_lt_prod_iff {ι : Type u_1} {M : Type u_4} [CommMonoid M] [PartialOrder M] [CanonicallyOrderedMul M] {f : ι → M} {s : Finset ι} :
1 < ∏ x ∈ s, f x ↔ ∃ x ∈ s, 1 < f x
source
theorem Finset.sum_pos_iff {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [CanonicallyOrderedAdd M] {f : ι → M} {s : Finset ι} :
0 < ∑ x ∈ s, f x ↔ ∃ x ∈ s, 0 < f x
source
theorem Finset.prod_lt_prod' {ι : Type u_1} {M : Type u_4} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {f g : ι → M} {s : Finset ι} (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
∏ i ∈ s, f i < ∏ i ∈ s, g i
source
theorem Finset.sum_lt_sum {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {f g : ι → M} {s : Finset ι} (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
∑ i ∈ s, f i < ∑ i ∈ s, g i
source
theorem Finset.prod_lt_prod_of_nonempty' {ι : Type u_1} {M : Type u_4} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {f g : ι → M} {s : Finset ι} (hs : s.Nonempty) (hlt : ∀ i ∈ s, f i < g i) :
∏ i ∈ s, f i < ∏ i ∈ s, g i

In an ordered commutative monoid, if each factor `f i` of one nontrivial finite product is strictly less than the corresponding factor `g i` of another nontrivial finite product, then `s.prod f < s.prod g`.

source
theorem Finset.sum_lt_sum_of_nonempty {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {f g : ι → M} {s : Finset ι} (hs : s.Nonempty) (hlt : ∀ i ∈ s, f i < g i) :
∑ i ∈ s, f i < ∑ i ∈ s, g i

In an ordered additive commutative monoid, if each summand `f i` of one nontrivial finite sum is strictly less than the corresponding summand `g i` of another nontrivial finite sum, then `s.sum f < s.sum g`.

source
theorem Finset.prod_lt_prod_of_subset' {ι : Type u_1} {M : Type u_4} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M} {s t : Finset ι} (h : s ⊆ t) {i : ι} (ht : i ∈ t) (hs : i ∉ s) (hlt : 1 < f i) (hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j) :
∏ j ∈ s, f j < ∏ j ∈ t, f j
source
theorem Finset.sum_lt_sum_of_subset {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {f : ι → M} {s t : Finset ι} (h : s ⊆ t) {i : ι} (ht : i ∈ t) (hs : i ∉ s) (hlt : 0 < f i) (hle : ∀ j ∈ t, j ∉ s → 0 ≤ f j) :
∑ j ∈ s, f j < ∑ j ∈ t, f j
source
theorem Finset.single_lt_prod' {ι : Type u_1} {M : Type u_4} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M} {s : Finset ι} {i j : ι} (hij : j ≠ i) (hi : i ∈ s) (hj : j ∈ s) (hlt : 1 < f j) (hle : ∀ k ∈ s, k ≠ i → 1 ≤ f k) :
f i < ∏ k ∈ s, f k
source
theorem Finset.single_lt_sum {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {f : ι → M} {s : Finset ι} {i j : ι} (hij : j ≠ i) (hi : i ∈ s) (hj : j ∈ s) (hlt : 0 < f j) (hle : ∀ k ∈ s, k ≠ i → 0 ≤ f k) :
f i < ∑ k ∈ s, f k
source
theorem Finset.one_lt_prod {ι : Type u_1} {M : Type u_4} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ i ∈ s, 1 < f i) (hs : s.Nonempty) :
1 < ∏ i ∈ s, f i
source
theorem Finset.sum_pos {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ i ∈ s, 0 < f i) (hs : s.Nonempty) :
0 < ∑ i ∈ s, f i
source
theorem Finset.prod_lt_one {ι : Type u_1} {M : Type u_4} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ i ∈ s, f i < 1) (hs : s.Nonempty) :
∏ i ∈ s, f i < 1
source
theorem Finset.sum_neg {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ i ∈ s, f i < 0) (hs : s.Nonempty) :
∑ i ∈ s, f i < 0
source
theorem Finset.one_lt_prod' {ι : Type u_1} {M : Type u_4} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ i ∈ s, 1 ≤ f i) (hs : ∃ i ∈ s, 1 < f i) :
1 < ∏ i ∈ s, f i
source
theorem Finset.sum_pos' {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ i ∈ s, 0 ≤ f i) (hs : ∃ i ∈ s, 0 < f i) :
0 < ∑ i ∈ s, f i
source
theorem Finset.prod_lt_one' {ι : Type u_1} {M : Type u_4} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ i ∈ s, f i ≤ 1) (hs : ∃ i ∈ s, f i < 1) :
∏ i ∈ s, f i < 1
source
theorem Finset.sum_neg' {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {f : ι → M} {s : Finset ι} (h : ∀ i ∈ s, f i ≤ 0) (hs : ∃ i ∈ s, f i < 0) :
∑ i ∈ s, f i < 0
source
theorem Finset.prod_eq_prod_iff_of_le {ι : Type u_1} {M : Type u_4} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {s : Finset ι} {f g : ι → M} (h : ∀ i ∈ s, f i ≤ g i) :
∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
source
theorem Finset.sum_eq_sum_iff_of_le {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {s : Finset ι} {f g : ι → M} (h : ∀ i ∈ s, f i ≤ g i) :
∑ i ∈ s, f i = ∑ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
source
theorem Finset.prod_sdiff_le_prod_sdiff {ι : Type u_1} {M : Type u_4} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M} {s t : Finset ι} [DecidableEq ι] :
∏ i ∈ s \ t, f i ≤ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i
source
theorem Finset.sum_sdiff_le_sum_sdiff {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {f : ι → M} {s t : Finset ι} [DecidableEq ι] :
∑ i ∈ s \ t, f i ≤ ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i ≤ ∑ i ∈ t, f i
source
theorem Finset.prod_sdiff_lt_prod_sdiff {ι : Type u_1} {M : Type u_4} [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M} {s t : Finset ι} [DecidableEq ι] :
∏ i ∈ s \ t, f i < ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i
source
theorem Finset.sum_sdiff_lt_sum_sdiff {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {f : ι → M} {s t : Finset ι} [DecidableEq ι] :
∑ i ∈ s \ t, f i < ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i < ∑ i ∈ t, f i
source
theorem Finset.exists_lt_of_prod_lt' {ι : Type u_1} {M : Type u_4} [CommMonoid M] [LinearOrder M] {f g : ι → M} {s : Finset ι} [MulLeftMono M] (Hlt : ∏ i ∈ s, f i < ∏ i ∈ s, g i) :
∃ i ∈ s, f i < g i
source
theorem Finset.exists_lt_of_sum_lt {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [LinearOrder M] {f g : ι → M} {s : Finset ι} [AddLeftMono M] (Hlt : ∑ i ∈ s, f i < ∑ i ∈ s, g i) :
∃ i ∈ s, f i < g i
source
theorem Finset.exists_le_of_prod_le' {ι : Type u_1} {M : Type u_4} [CommMonoid M] [LinearOrder M] {f g : ι → M} {s : Finset ι} [IsOrderedCancelMonoid M] (hs : s.Nonempty) (Hle : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i) :
∃ i ∈ s, f i ≤ g i
source
theorem Finset.exists_le_of_sum_le {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [LinearOrder M] {f g : ι → M} {s : Finset ι} [IsOrderedCancelAddMonoid M] (hs : s.Nonempty) (Hle : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i) :
∃ i ∈ s, f i ≤ g i
source
theorem Finset.exists_one_lt_of_prod_one_of_exists_ne_one' {ι : Type u_1} {M : Type u_4} [CommMonoid M] [LinearOrder M] {s : Finset ι} [IsOrderedCancelMonoid M] (f : ι → M) (h₁ : ∏ i ∈ s, f i = 1) (h₂ : ∃ i ∈ s, f i ≠ 1) :
∃ i ∈ s, 1 < f i
source
theorem Finset.exists_pos_of_sum_zero_of_exists_nonzero {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [LinearOrder M] {s : Finset ι} [IsOrderedCancelAddMonoid M] (f : ι → M) (h₁ : ∑ i ∈ s, f i = 0) (h₂ : ∃ i ∈ s, f i ≠ 0) :
∃ i ∈ s, 0 < f i
source
theorem Finset.apply_sup_le_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [SemilatticeSup α] [OrderBot α] [AddCommMonoid β] [PartialOrder β] [AddLeftMono β] {f : α → β} (zero : f ⊥ = 0) (ih : ∀ {s t : α}, f (s ⊔ t) ≤ f s + f t) {s : ι → α} (t : Finset ι) :
f (t.sup s) ≤ ∑ i ∈ t, f (s i)
source
theorem Finset.apply_union_le_sum {ι : Type u_1} {α : Type u_2} {β : Type u_3} [AddCommMonoid β] [PartialOrder β] [AddLeftMono β] {f : Set α → β} (zero : f ∅ = 0) (ih : ∀ {s t : Set α}, f (s ∪ t) ≤ f s + f t) {s : ι → Set α} (t : Finset ι) :
f (⋃ i ∈ t, s i) ≤ ∑ i ∈ t, f (s i)
source
theorem Fintype.prod_mono' {ι : Type u_1} {M : Type u_4} [Fintype ι] [CommMonoid M] [PartialOrder M] [MulLeftMono M] :
Monotone fun (f : ι → M) => ∏ i : ι, f i
source
theorem Fintype.sum_mono {ι : Type u_1} {M : Type u_4} [Fintype ι] [AddCommMonoid M] [PartialOrder M] [AddLeftMono M] :
Monotone fun (f : ι → M) => ∑ i : ι, f i
source
theorem Fintype.one_le_prod {ι : Type u_1} {M : Type u_4} [Fintype ι] [CommMonoid M] [PartialOrder M] [MulLeftMono M] {f : ι → M} (hf : 1 ≤ f) :
1 ≤ ∏ i : ι, f i
source
theorem Fintype.sum_nonneg {ι : Type u_1} {M : Type u_4} [Fintype ι] [AddCommMonoid M] [PartialOrder M] [AddLeftMono M] {f : ι → M} (hf : 0 ≤ f) :
0 ≤ ∑ i : ι, f i
source
theorem Fintype.prod_le_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [CommMonoid M] [PartialOrder M] [MulLeftMono M] {f : ι → M} (hf : f ≤ 1) :
∏ i : ι, f i ≤ 1
source
theorem Fintype.sum_nonpos {ι : Type u_1} {M : Type u_4} [Fintype ι] [AddCommMonoid M] [PartialOrder M] [AddLeftMono M] {f : ι → M} (hf : f ≤ 0) :
∑ i : ι, f i ≤ 0
source
theorem Fintype.prod_eq_one_iff_of_one_le {ι : Type u_1} {M : Type u_4} [Fintype ι] [CommMonoid M] [PartialOrder M] [MulLeftMono M] {f : ι → M} (hf : 1 ≤ f) :
∏ i : ι, f i = 1 ↔ f = 1
source
theorem Fintype.sum_eq_zero_iff_of_nonneg {ι : Type u_1} {M : Type u_4} [Fintype ι] [AddCommMonoid M] [PartialOrder M] [AddLeftMono M] {f : ι → M} (hf : 0 ≤ f) :
∑ i : ι, f i = 0 ↔ f = 0
source
theorem Fintype.prod_eq_one_iff_of_le_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [CommMonoid M] [PartialOrder M] [MulLeftMono M] {f : ι → M} (hf : f ≤ 1) :
∏ i : ι, f i = 1 ↔ f = 1
source
theorem Fintype.sum_eq_zero_iff_of_nonpos {ι : Type u_1} {M : Type u_4} [Fintype ι] [AddCommMonoid M] [PartialOrder M] [AddLeftMono M] {f : ι → M} (hf : f ≤ 0) :
∑ i : ι, f i = 0 ↔ f = 0
source
theorem Fintype.prod_strictMono' {ι : Type u_1} {M : Type u_4} [Fintype ι] [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] :
StrictMono fun (f : ι → M) => ∏ x : ι, f x
source
theorem Fintype.sum_strictMono {ι : Type u_1} {M : Type u_4} [Fintype ι] [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] :
StrictMono fun (f : ι → M) => ∑ x : ι, f x
source
theorem Fintype.one_lt_prod {ι : Type u_1} {M : Type u_4} [Fintype ι] [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M} (hf : 1 < f) :
1 < ∏ i : ι, f i
source
theorem Fintype.sum_pos {ι : Type u_1} {M : Type u_4} [Fintype ι] [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {f : ι → M} (hf : 0 < f) :
0 < ∑ i : ι, f i
source
theorem Fintype.prod_lt_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M} (hf : f < 1) :
∏ i : ι, f i < 1
source
theorem Fintype.sum_neg {ι : Type u_1} {M : Type u_4} [Fintype ι] [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {f : ι → M} (hf : f < 0) :
∑ i : ι, f i < 0
source
theorem Fintype.one_lt_prod_iff_of_one_le {ι : Type u_1} {M : Type u_4} [Fintype ι] [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M} (hf : 1 ≤ f) :
1 < ∏ i : ι, f i ↔ 1 < f
source
theorem Fintype.sum_pos_iff_of_nonneg {ι : Type u_1} {M : Type u_4} [Fintype ι] [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {f : ι → M} (hf : 0 ≤ f) :
0 < ∑ i : ι, f i ↔ 0 < f
source
theorem Fintype.prod_lt_one_iff_of_le_one {ι : Type u_1} {M : Type u_4} [Fintype ι] [CommMonoid M] [PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M} (hf : f ≤ 1) :
∏ i : ι, f i < 1 ↔ f < 1
source
theorem Fintype.sum_neg_iff_of_nonpos {ι : Type u_1} {M : Type u_4} [Fintype ι] [AddCommMonoid M] [PartialOrder M] [IsOrderedCancelAddMonoid M] {f : ι → M} (hf : f ≤ 0) :
∑ i : ι, f i < 0 ↔ f < 0
source
theorem Multiset.finset_sum_eq_sup_iff_disjoint {α : Type u_2} {β : Type u_3} [DecidableEq α] {i : Finset β} {f : β → Multiset α} :
i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → Disjoint (f x) (f y)
source
theorem Multiset.sup_powerset_len {α : Type u_2} [DecidableEq α] (x : Multiset α) :
((Finset.range (x.card + 1)).sup fun (k : ℕ) => powersetCard k x) = x.powerset