Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl

! This file was ported from Lean 3 source module algebra.big_operators.order
! leanprover-community/mathlib commit 824f9ae93a4f5174d2ea948e2d75843dd83447bb
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Order.AbsoluteValue
import Mathlib.Algebra.Order.Ring.WithTop
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Fintype.Card

/-!
# Results about big operators with values in an ordered algebraic structure.

Mostly monotonicity results for the `∏` and `∑` operations.

-/

open Function

open BigOperators

variable {
ι: Type ?u.26
ι
α: Type ?u.114554
α
β: Type ?u.75944
β
M: Type ?u.111508
M
N: Type ?u.38
N
G: Type ?u.114566
G
k: Type ?u.20
k
R: Type ?u.114572
R
:
Type _: Type (?u.114566+1)
Type _
} namespace Finset section OrderedCommMonoid variable [
CommMonoid: Type ?u.19646 → Type ?u.19646
CommMonoid
M: Type ?u.23981
M
] [
OrderedCommMonoid: Type ?u.15696 → Type ?u.15696
OrderedCommMonoid
N: Type ?u.38
N
] /-- 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 in s, g x) ≤ ∏ x in s, f (g x)`. -/ @[to_additive
le_sum_nonempty_of_subadditive_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N) (p : M → Prop), (∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) → (∀ (x y : M), p x → p y → p (x + y)) → ∀ (g : ι → M) (s : Finset ι), Finset.Nonempty s → (∀ (i : ι), i ∈ s → p (g i)) → f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
le_sum_nonempty_of_subadditive_on_pred
] theorem
le_prod_nonempty_of_submultiplicative_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N) (p : M → Prop), (∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) → (∀ (x y : M), p x → p y → p (x * y)) → ∀ (g : ι → M) (s : Finset ι), Finset.Nonempty s → (∀ (i : ι), i ∈ s → p (g i)) → f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
le_prod_nonempty_of_submultiplicative_on_pred
(
f: M → N
f
:
M: Type ?u.65
M
→
N: Type ?u.68
N
) (
p: M → Prop
p
:
M: Type ?u.65
M
→
Prop: Type
Prop
) (
h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
h_mul
: ∀
x: ?m.95
x
y: ?m.98
y
,
p: M → Prop
p
x: ?m.95
x
→
p: M → Prop
p
y: ?m.98
y
→
f: M → N
f
(
x: ?m.95
x
*
y: ?m.98
y
) ≤
f: M → N
f
x: ?m.95
x
*
f: M → N
f
y: ?m.98
y
) (
hp_mul: ∀ (x y : M), p x → p y → p (x * y)
hp_mul
: ∀
x: ?m.2274
x
y: ?m.2277
y
,
p: M → Prop
p
x: ?m.2274
x
→
p: M → Prop
p
y: ?m.2277
y
→
p: M → Prop
p
(
x: ?m.2274
x
*
y: ?m.2277
y
)) (
g: ι → M
g
:
ι: Type ?u.56
ι
→
M: Type ?u.65
M
) (
s: Finset ι
s
:
Finset: Type ?u.2705 → Type ?u.2705
Finset
ι: Type ?u.56
ι
) (
hs_nonempty: Finset.Nonempty s
hs_nonempty
:
s: Finset ι
s
.
Nonempty: {α : Type ?u.2708} → Finset α → Prop
Nonempty
) (
hs: ∀ (i : ι), i ∈ s → p (g i)
hs
: ∀
i: ?m.2716
i
∈
s: Finset ι
s
,
p: M → Prop
p
(
g: ι → M
g
i: ?m.2716
i
)) :
f: M → N
f
(∏
i: ?m.2781
i
in
s: Finset ι
s
,
g: ι → M
g
i: ?m.2781
i
) ≤ ∏
i: ?m.2803
i
in
s: Finset ι
s
,
f: M → N
f
(
g: ι → M
g
i: ?m.2803
i
) :=

Goals accomplished! 🐙
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


refine'_1
Multiset.map (fun i => g i) s.val ≠ ∅
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


refine'_2
∀ (a : M), a ∈ Multiset.map (fun i => g i) s.val → p a
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


refine'_3
Multiset.prod (Multiset.map f (Multiset.map (fun i => g i) s.val)) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


refine'_1
Multiset.map (fun i => g i) s.val ≠ ∅
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


refine'_1
Multiset.map (fun i => g i) s.val ≠ ∅
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


refine'_2
∀ (a : M), a ∈ Multiset.map (fun i => g i) s.val → p a
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


refine'_3
Multiset.prod (Multiset.map f (Multiset.map (fun i => g i) s.val)) ≤ ∏ i in s, f (g i)

Goals accomplished! 🐙
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


refine'_2
∀ (a : M), a ∈ Multiset.map (fun i => g i) s.val → p a
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


refine'_2
∀ (a : M), a ∈ Multiset.map (fun i => g i) s.val → p a
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


refine'_3
Multiset.prod (Multiset.map f (Multiset.map (fun i => g i) s.val)) ≤ ∏ i in s, f (g i)

Goals accomplished! 🐙
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


refine'_3
Multiset.prod (Multiset.map f (Multiset.map (fun i => g i) s.val)) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


refine'_3
Multiset.prod (Multiset.map (f ∘ fun i => g i) s.val) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


refine'_3
Multiset.prod (Multiset.map (f ∘ fun i => g i) s.val) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.59

β: Type ?u.62

M: Type u_2

N: Type u_1

G: Type ?u.71

k: Type ?u.74

R: Type ?u.77

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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: Finset.Nonempty s

hs: ∀ (i : ι), i ∈ s → p (g i)


f (∏ i in s, g i) ≤ ∏ i in s, f (g i)

Goals accomplished! 🐙
#align finset.le_prod_nonempty_of_submultiplicative_on_pred
Finset.le_prod_nonempty_of_submultiplicative_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N) (p : M → Prop), (∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) → (∀ (x y : M), p x → p y → p (x * y)) → ∀ (g : ι → M) (s : Finset ι), Finset.Nonempty s → (∀ (i : ι), i ∈ s → p (g i)) → f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
Finset.le_prod_nonempty_of_submultiplicative_on_pred
#align finset.le_sum_nonempty_of_subadditive_on_pred
Finset.le_sum_nonempty_of_subadditive_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N) (p : M → Prop), (∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) → (∀ (x y : M), p x → p y → p (x + y)) → ∀ (g : ι → M) (s : Finset ι), Finset.Nonempty s → (∀ (i : ι), i ∈ s → p (g i)) → f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
Finset.le_sum_nonempty_of_subadditive_on_pred
/-- 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 in s, g i) ≤ ∑ i in s, f (g i)`. -/ add_decl_doc
le_sum_nonempty_of_subadditive_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N) (p : M → Prop), (∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) → (∀ (x y : M), p x → p y → p (x + y)) → ∀ (g : ι → M) (s : Finset ι), Finset.Nonempty s → (∀ (i : ι), i ∈ s → p (g i)) → f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
le_sum_nonempty_of_subadditive_on_pred
/-- 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 in s, g i) ≤ ∏ i in s, f (g i)`. -/ @[to_additive
le_sum_nonempty_of_subadditive: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N), (∀ (x y : M), f (x + y) ≤ f x + f y) → ∀ {s : Finset ι}, Finset.Nonempty s → ∀ (g : ι → M), f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
le_sum_nonempty_of_subadditive
] theorem
le_prod_nonempty_of_submultiplicative: ∀ (f : M → N), (∀ (x y : M), f (x * y) ≤ f x * f y) → ∀ {s : Finset ι}, Finset.Nonempty s → ∀ (g : ι → M), f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
le_prod_nonempty_of_submultiplicative
(
f: M → N
f
:
M: Type ?u.3862
M
→
N: Type ?u.3865
N
) (
h_mul: ∀ (x y : M), f (x * y) ≤ f x * f y
h_mul
: ∀
x: ?m.3888
x
y: ?m.3891
y
,
f: M → N
f
(
x: ?m.3888
x
*
y: ?m.3891
y
) ≤
f: M → N
f
x: ?m.3888
x
*
f: M → N
f
y: ?m.3891
y
) {
s: Finset ι
s
:
Finset: Type ?u.6060 → Type ?u.6060
Finset
ι: Type ?u.3853
ι
} (hs :
s: Finset ι
s
.
Nonempty: {α : Type ?u.6063} → Finset α → Prop
Nonempty
) (
g: ι → M
g
:
ι: Type ?u.3853
ι
→
M: Type ?u.3862
M
) :
f: M → N
f
(∏
i: ?m.6104
i
in
s: Finset ι
s
,
g: ι → M
g
i: ?m.6104
i
) ≤ ∏
i: ?m.6126
i
in
s: Finset ι
s
,
f: M → N
f
(
g: ι → M
g
i: ?m.6126
i
) :=
le_prod_nonempty_of_submultiplicative_on_pred: ∀ {ι : Type ?u.6194} {M : Type ?u.6193} {N : Type ?u.6192} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N) (p : M → Prop), (∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) → (∀ (x y : M), p x → p y → p (x * y)) → ∀ (g : ι → M) (s : Finset ι), Finset.Nonempty s → (∀ (i : ι), i ∈ s → p (g i)) → f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
le_prod_nonempty_of_submultiplicative_on_pred
f: M → N
f
(fun
_: ?m.6204
_
↦
True: Prop
True
) (fun
x: ?m.6209
x
y: ?m.6212
y
_: ?m.6215
_
_: ?m.6218
_
↦
h_mul: ∀ (x y : M), f (x * y) ≤ f x * f y
h_mul
x: ?m.6209
x
y: ?m.6212
y
) (fun
_: ?m.6288
_
_: ?m.6291
_
_: ?m.6294
_
_: ?m.6297
_
↦
trivial: True
trivial
)
g: ι → M
g
s: Finset ι
s
hs fun
_: ?m.6314
_
_: ?m.6317
_
↦
trivial: True
trivial
#align finset.le_prod_nonempty_of_submultiplicative
Finset.le_prod_nonempty_of_submultiplicative: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N), (∀ (x y : M), f (x * y) ≤ f x * f y) → ∀ {s : Finset ι}, Finset.Nonempty s → ∀ (g : ι → M), f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
Finset.le_prod_nonempty_of_submultiplicative
#align finset.le_sum_nonempty_of_subadditive
Finset.le_sum_nonempty_of_subadditive: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N), (∀ (x y : M), f (x + y) ≤ f x + f y) → ∀ {s : Finset ι}, Finset.Nonempty s → ∀ (g : ι → M), f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
Finset.le_sum_nonempty_of_subadditive
/-- 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 in s, g i) ≤ ∑ i in s, f (g i)`. -/ add_decl_doc
le_sum_nonempty_of_subadditive: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N), (∀ (x y : M), f (x + y) ≤ f x + f y) → ∀ {s : Finset ι}, Finset.Nonempty s → ∀ (g : ι → M), f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
le_sum_nonempty_of_subadditive
/-- 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 in s, g i) ≤ ∏ i in s, f (g i)`. -/ @[to_additive
le_sum_of_subadditive_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N) (p : M → Prop), f 0 = 0 → (∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) → (∀ (x y : M), p x → p y → p (x + y)) → ∀ (g : ι → M) {s : Finset ι}, (∀ (i : ι), i ∈ s → p (g i)) → f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
le_sum_of_subadditive_on_pred
] theorem
le_prod_of_submultiplicative_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N) (p : M → Prop), f 1 = 1 → (∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) → (∀ (x y : M), p x → p y → p (x * y)) → ∀ (g : ι → M) {s : Finset ι}, (∀ (i : ι), i ∈ s → p (g i)) → f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
le_prod_of_submultiplicative_on_pred
(
f: M → N
f
:
M: Type ?u.6433
M
→
N: Type ?u.6436
N
) (
p: M → Prop
p
:
M: Type ?u.6433
M
→
Prop: Type
Prop
) (
h_one: f 1 = 1
h_one
:
f: M → N
f
1: ?m.6464
1
=
1: ?m.6944
1
) (
h_mul: ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
h_mul
: ∀
x: ?m.7462
x
y: ?m.7465
y
,
p: M → Prop
p
x: ?m.7462
x
→
p: M → Prop
p
y: ?m.7465
y
→
f: M → N
f
(
x: ?m.7462
x
*
y: ?m.7465
y
) ≤
f: M → N
f
x: ?m.7462
x
*
f: M → N
f
y: ?m.7465
y
) (
hp_mul: ∀ (x y : M), p x → p y → p (x * y)
hp_mul
: ∀
x: ?m.9455
x
y: ?m.9458
y
,
p: M → Prop
p
x: ?m.9455
x
→
p: M → Prop
p
y: ?m.9458
y
→
p: M → Prop
p
(
x: ?m.9455
x
*
y: ?m.9458
y
)) (
g: ι → M
g
:
ι: Type ?u.6424
ι
→
M: Type ?u.6433
M
) {
s: Finset ι
s
:
Finset: Type ?u.9886 → Type ?u.9886
Finset
ι: Type ?u.6424
ι
} (
hs: ∀ (i : ι), i ∈ s → p (g i)
hs
: ∀
i: ?m.9890
i
∈
s: Finset ι
s
,
p: M → Prop
p
(
g: ι → M
g
i: ?m.9890
i
)) :
f: M → N
f
(∏
i: ?m.9956
i
in
s: Finset ι
s
,
g: ι → M
g
i: ?m.9956
i
) ≤ ∏
i: ?m.9978
i
in
s: Finset ι
s
,
f: M → N
f
(
g: ι → M
g
i: ?m.9978
i
) :=

Goals accomplished! 🐙
ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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 : ι), i ∈ s → p (g i)


f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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

hs: ∀ (i : ι), i ∈ ∅ → p (g i)


inl
f (∏ i in ∅, g i) ≤ ∏ i in ∅, f (g i)
ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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 : ι), i ∈ s → p (g i)

hs_nonempty: Finset.Nonempty s


inr
f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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 : ι), i ∈ s → p (g i)


f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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

hs: ∀ (i : ι), i ∈ ∅ → p (g i)


inl
f (∏ i in ∅, g i) ≤ ∏ i in ∅, f (g i)
ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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

hs: ∀ (i : ι), i ∈ ∅ → p (g i)


inl
f (∏ i in ∅, g i) ≤ ∏ i in ∅, f (g i)
ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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 : ι), i ∈ s → p (g i)

hs_nonempty: Finset.Nonempty s


inr
f (∏ i in s, g i) ≤ ∏ i in s, f (g i)

Goals accomplished! 🐙
ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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 : ι), i ∈ s → p (g i)


f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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 : ι), i ∈ s → p (g i)

hs_nonempty: Finset.Nonempty s


inr
f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.6427

β: Type ?u.6430

M: Type u_2

N: Type u_1

G: Type ?u.6439

k: Type ?u.6442

R: Type ?u.6445

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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 : ι), i ∈ s → p (g i)

hs_nonempty: Finset.Nonempty s


inr
f (∏ i in s, g i) ≤ ∏ i in s, f (g i)

Goals accomplished! 🐙
#align finset.le_prod_of_submultiplicative_on_pred
Finset.le_prod_of_submultiplicative_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N) (p : M → Prop), f 1 = 1 → (∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y) → (∀ (x y : M), p x → p y → p (x * y)) → ∀ (g : ι → M) {s : Finset ι}, (∀ (i : ι), i ∈ s → p (g i)) → f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
Finset.le_prod_of_submultiplicative_on_pred
#align finset.le_sum_of_subadditive_on_pred
Finset.le_sum_of_subadditive_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N) (p : M → Prop), f 0 = 0 → (∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) → (∀ (x y : M), p x → p y → p (x + y)) → ∀ (g : ι → M) {s : Finset ι}, (∀ (i : ι), i ∈ s → p (g i)) → f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
Finset.le_sum_of_subadditive_on_pred
/-- 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 in s, g x) ≤ ∑ x in s, f (g x)`. -/ add_decl_doc
le_sum_of_subadditive_on_pred: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N) (p : M → Prop), f 0 = 0 → (∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y) → (∀ (x y : M), p x → p y → p (x + y)) → ∀ (g : ι → M) {s : Finset ι}, (∀ (i : ι), i ∈ s → p (g i)) → f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
le_sum_of_subadditive_on_pred
/-- 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 in s, g i) ≤ ∏ i in s, f (g i)`. -/ @[to_additive
le_sum_of_subadditive: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N), f 0 = 0 → (∀ (x y : M), f (x + y) ≤ f x + f y) → ∀ (s : Finset ι) (g : ι → M), f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
le_sum_of_subadditive
] theorem
le_prod_of_submultiplicative: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N), f 1 = 1 → (∀ (x y : M), f (x * y) ≤ f x * f y) → ∀ (s : Finset ι) (g : ι → M), f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
le_prod_of_submultiplicative
(
f: M → N
f
:
M: Type ?u.11331
M
→
N: Type ?u.11334
N
) (
h_one: f 1 = 1
h_one
:
f: M → N
f
1: ?m.11358
1
=
1: ?m.11838
1
) (
h_mul: ∀ (x y : M), f (x * y) ≤ f x * f y
h_mul
: ∀
x: ?m.12356
x
y: ?m.12359
y
,
f: M → N
f
(
x: ?m.12356
x
*
y: ?m.12359
y
) ≤
f: M → N
f
x: ?m.12356
x
*
f: M → N
f
y: ?m.12359
y
) (
s: Finset ι
s
:
Finset: Type ?u.14342 → Type ?u.14342
Finset
ι: Type ?u.11322
ι
) (
g: ι → M
g
:
ι: Type ?u.11322
ι
→
M: Type ?u.11331
M
) :
f: M → N
f
(∏
i: ?m.14380
i
in
s: Finset ι
s
,
g: ι → M
g
i: ?m.14380
i
) ≤ ∏
i: ?m.14402
i
in
s: Finset ι
s
,
f: M → N
f
(
g: ι → M
g
i: ?m.14402
i
) :=

Goals accomplished! 🐙
ι: Type u_3

α: Type ?u.11325

β: Type ?u.11328

M: Type u_2

N: Type u_1

G: Type ?u.11337

k: Type ?u.11340

R: Type ?u.11343

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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 in s, g i) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.11325

β: Type ?u.11328

M: Type u_2

N: Type u_1

G: Type ?u.11337

k: Type ?u.11340

R: Type ?u.11343

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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


Multiset.prod (Multiset.map f (Multiset.map (fun i => g i) s.val)) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.11325

β: Type ?u.11328

M: Type u_2

N: Type u_1

G: Type ?u.11337

k: Type ?u.11340

R: Type ?u.11343

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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 in s, g i) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.11325

β: Type ?u.11328

M: Type u_2

N: Type u_1

G: Type ?u.11337

k: Type ?u.11340

R: Type ?u.11343

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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


Multiset.prod (Multiset.map f (Multiset.map (fun i => g i) s.val)) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.11325

β: Type ?u.11328

M: Type u_2

N: Type u_1

G: Type ?u.11337

k: Type ?u.11340

R: Type ?u.11343

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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


Multiset.prod (Multiset.map (f ∘ fun i => g i) s.val) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.11325

β: Type ?u.11328

M: Type u_2

N: Type u_1

G: Type ?u.11337

k: Type ?u.11340

R: Type ?u.11343

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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


Multiset.prod (Multiset.map (f ∘ fun i => g i) s.val) ≤ ∏ i in s, f (g i)
ι: Type u_3

α: Type ?u.11325

β: Type ?u.11328

M: Type u_2

N: Type u_1

G: Type ?u.11337

k: Type ?u.11340

R: Type ?u.11343

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid 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 in s, g i) ≤ ∏ i in s, f (g i)

Goals accomplished! 🐙
#align finset.le_prod_of_submultiplicative
Finset.le_prod_of_submultiplicative: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : CommMonoid M] [inst_1 : OrderedCommMonoid N] (f : M → N), f 1 = 1 → (∀ (x y : M), f (x * y) ≤ f x * f y) → ∀ (s : Finset ι) (g : ι → M), f (∏ i in s, g i) ≤ ∏ i in s, f (g i)
Finset.le_prod_of_submultiplicative
#align finset.le_sum_of_subadditive
Finset.le_sum_of_subadditive: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N), f 0 = 0 → (∀ (x y : M), f (x + y) ≤ f x + f y) → ∀ (s : Finset ι) (g : ι → M), f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
Finset.le_sum_of_subadditive
/-- 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 in s, g i) ≤ ∑ i in s, f (g i)`. -/ add_decl_doc
le_sum_of_subadditive: ∀ {ι : Type u_3} {M : Type u_2} {N : Type u_1} [inst : AddCommMonoid M] [inst_1 : OrderedAddCommMonoid N] (f : M → N), f 0 = 0 → (∀ (x y : M), f (x + y) ≤ f x + f y) → ∀ (s : Finset ι) (g : ι → M), f (∑ i in s, g i) ≤ ∑ i in s, f (g i)
le_sum_of_subadditive
variable {
f: ι → N
f
g: ι → N
g
:
ι: Type ?u.15056
ι
→
N: Type ?u.15068
N
} {
s: Finset ι
s
t: Finset ι
t
:
Finset: Type ?u.19663 → Type ?u.19663
Finset
ι: Type ?u.15056
ι
} /-- 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 in s, f i ≤ ∏ i in s, g i`. -/ @[to_additive
sum_le_sum: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f g : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → f i ≤ g i) → ∑ i in s, f i ≤ ∑ i in s, g i
sum_le_sum
] theorem
prod_le_prod': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f g : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
prod_le_prod'
(
h: ∀ (i : ι), i ∈ s → f i ≤ g i
h
: ∀
i: ?m.15145
i
∈
s: Finset ι
s
,
f: ι → N
f
i: ?m.15145
i
≤
g: ι → N
g
i: ?m.15145
i
) : (∏
i: ?m.15478
i
in
s: Finset ι
s
,
f: ι → N
f
i: ?m.15478
i
) ≤ ∏
i: ?m.15542
i
in
s: Finset ι
s
,
g: ι → N
g
i: ?m.15542
i
:=
Multiset.prod_map_le_prod_map: ∀ {ι : Type ?u.15553} {α : Type ?u.15554} [inst : OrderedCommMonoid α] {s : Multiset ι} (f g : ι → α), (∀ (i : ι), i ∈ s → f i ≤ g i) → Multiset.prod (Multiset.map f s) ≤ Multiset.prod (Multiset.map g s)
Multiset.prod_map_le_prod_map
f: ι → N
f
g: ι → N
g
h: ∀ (i : ι), i ∈ s → f i ≤ g i
h
#align finset.prod_le_prod'
Finset.prod_le_prod': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f g : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
Finset.prod_le_prod'
#align finset.sum_le_sum
Finset.sum_le_sum: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f g : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → f i ≤ g i) → ∑ i in s, f i ≤ ∑ i in s, g i
Finset.sum_le_sum
/-- 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 in s, f i ≤ ∑ i in s, g i`. -/ add_decl_doc
sum_le_sum: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f g : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → f i ≤ g i) → ∑ i in s, f i ≤ ∑ i in s, g i
sum_le_sum
@[to_additive
sum_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → 0 ≤ f i) → 0 ≤ ∑ i in s, f i
sum_nonneg
] theorem
one_le_prod': (∀ (i : ι), i ∈ s → 1 ≤ f i) → 1 ≤ ∏ i in s, f i
one_le_prod'
(
h: ∀ (i : ι), i ∈ s → 1 ≤ f i
h
: ∀
i: ?m.15714
i
∈
s: Finset ι
s
,
1: ?m.15750
1
≤
f: ι → N
f
i: ?m.15714
i
) :
1: ?m.16526
1
≤ ∏
i: ?m.16548
i
in
s: Finset ι
s
,
f: ι → N
f
i: ?m.16548
i
:=
le_trans: ∀ {α : Type ?u.16611} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
le_trans
(

Goals accomplished! 🐙
ι: Type u_1

α: Type ?u.15672

β: Type ?u.15675

M: Type ?u.15678

N: Type u_2

G: Type ?u.15684

k: Type ?u.15687

R: Type ?u.15690

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: ∀ (i : ι), i ∈ s → 1 ≤ f i


1 ≤ ∏ i in s, 1
ι: Type u_1

α: Type ?u.15672

β: Type ?u.15675

M: Type ?u.15678

N: Type u_2

G: Type ?u.15684

k: Type ?u.15687

R: Type ?u.15690

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: ∀ (i : ι), i ∈ s → 1 ≤ f i


1 ≤ ∏ i in s, 1
ι: Type u_1

α: Type ?u.15672

β: Type ?u.15675

M: Type ?u.15678

N: Type u_2

G: Type ?u.15684

k: Type ?u.15687

R: Type ?u.15690

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: ∀ (i : ι), i ∈ s → 1 ≤ f i


1 ≤ 1

Goals accomplished! 🐙
) (
prod_le_prod': ∀ {ι : Type ?u.16924} {N : Type ?u.16925} [inst : OrderedCommMonoid N] {f g : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
prod_le_prod'
h: ∀ (i : ι), i ∈ s → 1 ≤ f i
h
) #align finset.one_le_prod'
Finset.one_le_prod': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → 1 ≤ f i) → 1 ≤ ∏ i in s, f i
Finset.one_le_prod'
#align finset.sum_nonneg
Finset.sum_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → 0 ≤ f i) → 0 ≤ ∑ i in s, f i
Finset.sum_nonneg
@[to_additive
Finset.sum_nonneg': ∀ {ι : Type u_2} {N : Type u_1} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), 0 ≤ f i) → 0 ≤ ∑ i in s, f i
Finset.sum_nonneg'
] theorem
one_le_prod'': ∀ {ι : Type u_2} {N : Type u_1} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), 1 ≤ f i) → 1 ≤ ∏ i in s, f i
one_le_prod''
(
h: ∀ (i : ι), 1 ≤ f i
h
: ∀
i: ι
i
:
ι: Type ?u.17163
ι
,
1: ?m.17212
1
≤
f: ι → N
f
i: ι
i
) :
1: ?m.17987
1
≤ ∏
i: ι
i
:
ι: Type ?u.17163
ι
in
s: Finset ι
s
,
f: ι → N
f
i: ι
i
:=
Finset.one_le_prod': ∀ {ι : Type ?u.18071} {N : Type ?u.18072} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → 1 ≤ f i) → 1 ≤ ∏ i in s, f i
Finset.one_le_prod'
fun
i: ?m.18119
i
_: ?m.18122
_
↦
h: ∀ (i : ι), 1 ≤ f i
h
i: ?m.18119
i
#align finset.one_le_prod''
Finset.one_le_prod'': ∀ {ι : Type u_2} {N : Type u_1} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), 1 ≤ f i) → 1 ≤ ∏ i in s, f i
Finset.one_le_prod''
#align finset.sum_nonneg'
Finset.sum_nonneg': ∀ {ι : Type u_2} {N : Type u_1} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), 0 ≤ f i) → 0 ≤ ∑ i in s, f i
Finset.sum_nonneg'
@[to_additive
sum_nonpos: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → f i ≤ 0) → ∑ i in s, f i ≤ 0
sum_nonpos
] theorem
prod_le_one': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → f i ≤ 1) → ∏ i in s, f i ≤ 1
prod_le_one'
(
h: ∀ (i : ι), i ∈ s → f i ≤ 1
h
: ∀
i: ?m.18224
i
∈
s: Finset ι
s
,
f: ι → N
f
i: ?m.18224
i
≤
1: ?m.18260
1
) : (∏
i: ?m.19037
i
in
s: Finset ι
s
,
f: ι → N
f
i: ?m.19037
i
) ≤
1: ?m.19089
1
:= (
prod_le_prod': ∀ {ι : Type ?u.19111} {N : Type ?u.19112} [inst : OrderedCommMonoid N] {f g : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → f i ≤ g i) → ∏ i in s, f i ≤ ∏ i in s, g i
prod_le_prod'
h: ∀ (i : ι), i ∈ s → f i ≤ 1
h
).
trans_eq: ∀ {α : Type ?u.19145} [inst : Preorder α] {a b c : α}, a ≤ b → b = c → a ≤ c
trans_eq
(

Goals accomplished! 🐙
ι: Type u_1

α: Type ?u.18182

β: Type ?u.18185

M: Type ?u.18188

N: Type u_2

G: Type ?u.18194

k: Type ?u.18197

R: Type ?u.18200

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: ∀ (i : ι), i ∈ s → f i ≤ 1


∏ i in s, 1 = 1
ι: Type u_1

α: Type ?u.18182

β: Type ?u.18185

M: Type ?u.18188

N: Type u_2

G: Type ?u.18194

k: Type ?u.18197

R: Type ?u.18200

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: ∀ (i : ι), i ∈ s → f i ≤ 1


∏ i in s, 1 = 1
ι: Type u_1

α: Type ?u.18182

β: Type ?u.18185

M: Type ?u.18188

N: Type u_2

G: Type ?u.18194

k: Type ?u.18197

R: Type ?u.18200

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: ∀ (i : ι), i ∈ s → f i ≤ 1


1 = 1

Goals accomplished! 🐙
) #align finset.prod_le_one'
Finset.prod_le_one': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → f i ≤ 1) → ∏ i in s, f i ≤ 1
Finset.prod_le_one'
#align finset.sum_nonpos
Finset.sum_nonpos: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → f i ≤ 0) → ∑ i in s, f i ≤ 0
Finset.sum_nonpos
@[to_additive
sum_le_sum_of_subset_of_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s t : Finset ι}, s ⊆ t → (∀ (i : ι), i ∈ t → ¬i ∈ s → 0 ≤ f i) → ∑ i in s, f i ≤ ∑ i in t, f i
sum_le_sum_of_subset_of_nonneg
] theorem
prod_le_prod_of_subset_of_one_le': s ⊆ t → (∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i) → ∏ i in s, f i ≤ ∏ i in t, f i
prod_le_prod_of_subset_of_one_le'
(
h: s ⊆ t
h
:
s: Finset ι
s
⊆
t: Finset ι
t
) (
hf: ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i
hf
: ∀
i: ?m.19686
i
∈
t: Finset ι
t
,
i: ?m.19686
i
∉
s: Finset ι
s
→
1: ?m.19733
1
≤
f: ι → N
f
i: ?m.19686
i
) : (∏
i: ?m.20516
i
in
s: Finset ι
s
,
f: ι → N
f
i: ?m.20516
i
) ≤ ∏
i: ?m.20574
i
in
t: Finset ι
t
,
f: ι → N
f
i: ?m.20574
i
:=

Goals accomplished! 🐙
ι: Type u_1

α: Type ?u.19625

β: Type ?u.19628

M: Type ?u.19631

N: Type u_2

G: Type ?u.19637

k: Type ?u.19640

R: Type ?u.19643

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: s ⊆ t

hf: ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i


∏ i in s, f i ≤ ∏ i in t, f i
ι: Type u_1

α: Type ?u.19625

β: Type ?u.19628

M: Type ?u.19631

N: Type u_2

G: Type ?u.19637

k: Type ?u.19640

R: Type ?u.19643

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: s ⊆ t

hf: ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i


∏ i in s, f i ≤ ∏ i in t, f i
ι: Type u_1

α: Type ?u.19625

β: Type ?u.19628

M: Type ?u.19631

N: Type u_2

G: Type ?u.19637

k: Type ?u.19640

R: Type ?u.19643

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: s ⊆ t

hf: ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i


∏ i in s, f i ≤ ∏ i in t, f i

Goals accomplished! 🐙
ι: Type u_1

α: Type ?u.19625

β: Type ?u.19628

M: Type ?u.19631

N: Type u_2

G: Type ?u.19637

k: Type ?u.19640

R: Type ?u.19643

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: s ⊆ t

hf: ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i


∀ (i : ι), i ∈ t \ s → 1 ≤ f i

Goals accomplished! 🐙
ι: Type u_1

α: Type ?u.19625

β: Type ?u.19628

M: Type ?u.19631

N: Type u_2

G: Type ?u.19637

k: Type ?u.19640

R: Type ?u.19643

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: s ⊆ t

hf: ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i


∏ i in s, f i ≤ ∏ i in t, f i

Goals accomplished! 🐙
ι: Type u_1

α: Type ?u.19625

β: Type ?u.19628

M: Type ?u.19631

N: Type u_2

G: Type ?u.19637

k: Type ?u.19640

R: Type ?u.19643

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: s ⊆ t

hf: ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i


∏ i in t \ s ∪ s, f i = ∏ i in t, f i
ι: Type u_1

α: Type ?u.19625

β: Type ?u.19628

M: Type ?u.19631

N: Type u_2

G: Type ?u.19637

k: Type ?u.19640

R: Type ?u.19643

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: s ⊆ t

hf: ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i


∏ i in t \ s ∪ s, f i = ∏ i in t, f i
ι: Type u_1

α: Type ?u.19625

β: Type ?u.19628

M: Type ?u.19631

N: Type u_2

G: Type ?u.19637

k: Type ?u.19640

R: Type ?u.19643

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι

h: s ⊆ t

hf: ∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i


∏ i in t, f i = ∏ i in t, f i

Goals accomplished! 🐙
#align finset.prod_le_prod_of_subset_of_one_le'
Finset.prod_le_prod_of_subset_of_one_le': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s t : Finset ι}, s ⊆ t → (∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i) → ∏ i in s, f i ≤ ∏ i in t, f i
Finset.prod_le_prod_of_subset_of_one_le'
#align finset.sum_le_sum_of_subset_of_nonneg
Finset.sum_le_sum_of_subset_of_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s t : Finset ι}, s ⊆ t → (∀ (i : ι), i ∈ t → ¬i ∈ s → 0 ≤ f i) → ∑ i in s, f i ≤ ∑ i in t, f i
Finset.sum_le_sum_of_subset_of_nonneg
@[to_additive
sum_mono_set_of_nonneg: ∀ {ι : Type u_2} {N : Type u_1} [inst : OrderedAddCommMonoid N] {f : ι → N}, (∀ (x : ι), 0 ≤ f x) → Monotone fun s => ∑ x in s, f x
sum_mono_set_of_nonneg
] theorem
prod_mono_set_of_one_le': (∀ (x : ι), 1 ≤ f x) → Monotone fun s => ∏ x in s, f x
prod_mono_set_of_one_le'
(
hf: ∀ (x : ι), 1 ≤ f x
hf
: ∀
x: ?m.24017
x
,
1: ?m.24022
1
≤
f: ι → N
f
x: ?m.24017
x
) :
Monotone: {α : Type ?u.24796} → {β : Type ?u.24795} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone
fun
s: ?m.24850
s
↦ ∏
x: ?m.24883
x
in
s: ?m.24850
s
,
f: ι → N
f
x: ?m.24883
x
:= fun
_: ?m.25180
_
_: ?m.25183
_
hst: ?m.25186
hst
↦
prod_le_prod_of_subset_of_one_le': ∀ {ι : Type ?u.25188} {N : Type ?u.25189} [inst : OrderedCommMonoid N] {f : ι → N} {s t : Finset ι}, s ⊆ t → (∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i) → ∏ i in s, f i ≤ ∏ i in t, f i
prod_le_prod_of_subset_of_one_le'
hst: ?m.25186
hst
fun
x: ?m.25233
x
_: ?m.25236
_
_: ?m.25239
_
↦
hf: ∀ (x : ι), 1 ≤ f x
hf
x: ?m.25233
x
#align finset.prod_mono_set_of_one_le'
Finset.prod_mono_set_of_one_le': ∀ {ι : Type u_2} {N : Type u_1} [inst : OrderedCommMonoid N] {f : ι → N}, (∀ (x : ι), 1 ≤ f x) → Monotone fun s => ∏ x in s, f x
Finset.prod_mono_set_of_one_le'
#align finset.sum_mono_set_of_nonneg
Finset.sum_mono_set_of_nonneg: ∀ {ι : Type u_2} {N : Type u_1} [inst : OrderedAddCommMonoid N] {f : ι → N}, (∀ (x : ι), 0 ≤ f x) → Monotone fun s => ∑ x in s, f x
Finset.sum_mono_set_of_nonneg
@[to_additive
sum_le_univ_sum_of_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} [inst_1 : Fintype ι] {s : Finset ι}, (∀ (x : ι), 0 ≤ f x) → ∑ x in s, f x ≤ ∑ x : ι, f x
sum_le_univ_sum_of_nonneg
] theorem
prod_le_univ_prod_of_one_le': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} [inst_1 : Fintype ι] {s : Finset ι}, (∀ (x : ι), 1 ≤ f x) → ∏ x in s, f x ≤ ∏ x : ι, f x
prod_le_univ_prod_of_one_le'
[
Fintype: Type ?u.25363 → Type ?u.25363
Fintype
ι: Type ?u.25319
ι
] {
s: Finset ι
s
:
Finset: Type ?u.25366 → Type ?u.25366
Finset
ι: Type ?u.25319
ι
} (
w: ∀ (x : ι), 1 ≤ f x
w
: ∀
x: ?m.25370
x
,
1: ?m.25375
1
≤
f: ι → N
f
x: ?m.25370
x
) : (∏
x: ?m.26157
x
in
s: Finset ι
s
,
f: ι → N
f
x: ?m.26157
x
) ≤ ∏
x: ?m.26266
x
,
f: ι → N
f
x: ?m.26266
x
:=
prod_le_prod_of_subset_of_one_le': ∀ {ι : Type ?u.26284} {N : Type ?u.26285} [inst : OrderedCommMonoid N] {f : ι → N} {s t : Finset ι}, s ⊆ t → (∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i) → ∏ i in s, f i ≤ ∏ i in t, f i
prod_le_prod_of_subset_of_one_le'
(
subset_univ: ∀ {α : Type ?u.26327} [inst : Fintype α] (s : Finset α), s ⊆ univ
subset_univ
s: Finset ι
s
) fun
a: ?m.26336
a
_: ?m.26339
_
_: ?m.26342
_
↦
w: ∀ (x : ι), 1 ≤ f x
w
a: ?m.26336
a
#align finset.prod_le_univ_prod_of_one_le'
Finset.prod_le_univ_prod_of_one_le': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} [inst_1 : Fintype ι] {s : Finset ι}, (∀ (x : ι), 1 ≤ f x) → ∏ x in s, f x ≤ ∏ x : ι, f x
Finset.prod_le_univ_prod_of_one_le'
#align finset.sum_le_univ_sum_of_nonneg
Finset.sum_le_univ_sum_of_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} [inst_1 : Fintype ι] {s : Finset ι}, (∀ (x : ι), 0 ≤ f x) → ∑ x in s, f x ≤ ∑ x : ι, f x
Finset.sum_le_univ_sum_of_nonneg
-- Porting Note: TODO -- The two next lemmas give the same lemma in additive version @[to_additive
sum_eq_zero_iff_of_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∑ i in s, f i = 0 ↔ ∀ (i : ι), i ∈ s → f i = 0)
sum_eq_zero_iff_of_nonneg
] theorem
prod_eq_one_iff_of_one_le': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
prod_eq_one_iff_of_one_le'
: (∀
i: ?m.26455
i
∈
s: Finset ι
s
,
1: ?m.26491
1
≤
f: ι → N
f
i: ?m.26455
i
) → ((∏
i: ?m.27270
i
in
s: Finset ι
s
,
f: ι → N
f
i: ?m.27270
i
) =
1: ?m.27322
1
↔ ∀
i: ?m.27339
i
∈
s: Finset ι
s
,
f: ι → N
f
i: ?m.27339
i
=
1: ?m.27371
1
) :=

Goals accomplished! 🐙
ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι


(∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι


(∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι


∀ ⦃a : ι⦄ {s : Finset ι}, ¬a ∈ s → ((∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)) → (∀ (i : ι), i ∈ insert a s → 1 ≤ f i) → (∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1)
ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι


(∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i


∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1
ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι


(∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i


∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1
ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s, t: Finset ι


(∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i


∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1
ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i


f a * ∏ x in s, f x = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1
ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i


∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1
ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i


f a = 1 ∧ ∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1
ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i


∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1
ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i


f a = 1 ∧ ∏ i in s, f i = 1 ↔ f a = 1 ∧ ∀ (x : ι), x ∈ s → f x = 1
ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i


∏ i in insert a s, f i = 1 ↔ ∀ (i : ι), i ∈ insert a s → f i = 1
ι: Type u_1

α: Type ?u.26412

β: Type ?u.26415

M: Type ?u.26418

N: Type u_2

G: Type ?u.26424

k: Type ?u.26427

R: Type ?u.26430

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f, g: ι → N

s✝, t: Finset ι

a: ι

s: Finset ι

ha: ¬a ∈ s

ih: (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)

H: ∀ (i : ι), i ∈ insert a s → 1 ≤ f i

this: ∀ (i : ι), i ∈ s → 1 ≤ f i


(f a = 1 ∧ ∀ (i : ι), i ∈ s → f i = 1) ↔ f a = 1 ∧ ∀ (x : ι), x ∈ s → f x = 1

Goals accomplished! 🐙
#align finset.prod_eq_one_iff_of_one_le'
Finset.prod_eq_one_iff_of_one_le': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
Finset.prod_eq_one_iff_of_one_le'
#align finset.sum_eq_zero_iff_of_nonneg
Finset.sum_eq_zero_iff_of_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∑ i in s, f i = 0 ↔ ∀ (i : ι), i ∈ s → f i = 0)
Finset.sum_eq_zero_iff_of_nonneg
@[to_additive existing
sum_eq_zero_iff_of_nonneg: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → 0 ≤ f i) → (∑ i in s, f i = 0 ↔ ∀ (i : ι), i ∈ s → f i = 0)
sum_eq_zero_iff_of_nonneg
] theorem
prod_eq_one_iff_of_le_one': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → f i ≤ 1) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
prod_eq_one_iff_of_le_one'
: (∀
i: ?m.30046
i
∈
s: Finset ι
s
,
f: ι → N
f
i: ?m.30046
i
≤
1: ?m.30082
1
) → ((∏
i: ?m.30856
i
in
s: Finset ι
s
,
f: ι → N
f
i: ?m.30856
i
) =
1: ?m.30908
1
↔ ∀
i: ?m.30925
i
∈
s: Finset ι
s
,
f: ι → N
f
i: ?m.30925
i
=
1: ?m.30957
1
) := @
prod_eq_one_iff_of_one_le': ∀ {ι : Type ?u.30976} {N : Type ?u.30977} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → 1 ≤ f i) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
prod_eq_one_iff_of_one_le'
_: Type ?u.30976
_
N: Type ?u.30012
N
ᵒᵈ _
_: ?m.30978 → Nᵒᵈ
_
_: Finset ?m.30978
_
#align finset.prod_eq_one_iff_of_le_one'
Finset.prod_eq_one_iff_of_le_one': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → f i ≤ 1) → (∏ i in s, f i = 1 ↔ ∀ (i : ι), i ∈ s → f i = 1)
Finset.prod_eq_one_iff_of_le_one'
-- Porting note: there is no align for the additive version since it aligns to the -- same one as the previous lemma @[to_additive
single_le_sum: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → 0 ≤ f i) → ∀ {a : ι}, a ∈ s → f a ≤ ∑ x in s, f x
single_le_sum
] theorem
single_le_prod': (∀ (i : ι), i ∈ s → 1 ≤ f i) → ∀ {a : ι}, a ∈ s → f a ≤ ∏ x in s, f x
single_le_prod'
(
hf: ∀ (i : ι), i ∈ s → 1 ≤ f i
hf
: ∀
i: ?m.31102
i
∈
s: Finset ι
s
,
1: ?m.31138
1
≤
f: ι → N
f
i: ?m.31102
i
) {
a: ι
a
} (
h: a ∈ s
h
:
a: ?m.31912
a
∈
s: Finset ι
s
) :
f: ι → N
f
a: ?m.31912
a
≤ ∏
x: ?m.31950
x
in
s: Finset ι
s
,
f: ι → N
f
x: ?m.31950
x
:= calc
f: ι → N
f
a: ι
a
= ∏
i: ?m.32047
i
in {
a: ι
a
},
f: ι → N
f
i: ?m.32047
i
:=
prod_singleton: ∀ {β : Type ?u.32117} {α : Type ?u.32116} {a : α} {f : α → β} [inst : CommMonoid β], ∏ x in {a}, f x = f a
prod_singleton
.
symm: ∀ {α : Sort ?u.32145} {a b : α}, a = b → b = a
symm
_: ?m✝
_
≤ ∏
i: ?m.32178
i
in
s: Finset ι
s
,
f: ι → N
f
i: ?m.32178
i
:=
prod_le_prod_of_subset_of_one_le': ∀ {ι : Type ?u.32456} {N : Type ?u.32457} [inst : OrderedCommMonoid N] {f : ι → N} {s t : Finset ι}, s ⊆ t → (∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i) → ∏ i in s, f i ≤ ∏ i in t, f i
prod_le_prod_of_subset_of_one_le'
(
singleton_subset_iff: ∀ {α : Type ?u.32490} {s : Finset α} {a : α}, {a} ⊆ s ↔ a ∈ s
singleton_subset_iff
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
h: a ∈ s
h
) fun
i: ?m.32511
i
hi: ?m.32514
hi
_: ?m.32517
_
↦
hf: ∀ (i : ι), i ∈ s → 1 ≤ f i
hf
i: ?m.32511
i
hi: ?m.32514
hi
#align finset.single_le_prod'
Finset.single_le_prod': ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → 1 ≤ f i) → ∀ {a : ι}, a ∈ s → f a ≤ ∏ x in s, f x
Finset.single_le_prod'
#align finset.single_le_sum
Finset.single_le_sum: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] {f : ι → N} {s : Finset ι}, (∀ (i : ι), i ∈ s → 0 ≤ f i) → ∀ {a : ι}, a ∈ s → f a ≤ ∑ x in s, f x
Finset.single_le_sum
@[to_additive
sum_le_card_nsmul: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] (s : Finset ι) (f : ι → N) (n : N), (∀ (x : ι), x ∈ s → f x ≤ n) → Finset.sum s f ≤ card s • n
sum_le_card_nsmul
] theorem
prod_le_pow_card: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] (s : Finset ι) (f : ι → N) (n : N), (∀ (x : ι), x ∈ s → f x ≤ n) → Finset.prod s f ≤ n ^ card s
prod_le_pow_card
(
s: Finset ι
s
:
Finset: Type ?u.32708 → Type ?u.32708
Finset
ι: Type ?u.32664
ι
) (
f: ι → N
f
:
ι: Type ?u.32664
ι
→
N: Type ?u.32676
N
) (
n: N
n
:
N: Type ?u.32676
N
) (
h: ∀ (x : ι), x ∈ s → f x ≤ n
h
: ∀
x: ?m.32718
x
∈
s: Finset ι
s
,
f: ι → N
f
x: ?m.32718
x
≤
n: N
n
) :
s: Finset ι
s
.
prod: {β : Type ?u.33045} → {α : Type ?u.33044} → [inst : CommMonoid β] → Finset α → (α → β) → β
prod
f: ι → N
f
≤
n: N
n
^
s: Finset ι
s
.
card: {α : Type ?u.33113} → Finset α → ℕ
card
:=

Goals accomplished! 🐙
ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n


ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n


refine'_1
∀ (x : N), x ∈ Multiset.map f s.val → x ≤ n
ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n


refine'_2
n ^ ↑Multiset.card (Multiset.map f s.val) ≤ n ^ card s
ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n


ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n


refine'_1
∀ (x : N), x ∈ Multiset.map f s.val → x ≤ n
ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n


refine'_1
∀ (x : N), x ∈ Multiset.map f s.val → x ≤ n
ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n


refine'_2
n ^ ↑Multiset.card (Multiset.map f s.val) ≤ n ^ card s

Goals accomplished! 🐙
ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n


ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n


refine'_2
n ^ ↑Multiset.card (Multiset.map f s.val) ≤ n ^ card s
ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n


refine'_2
n ^ ↑Multiset.card (Multiset.map f s.val) ≤ n ^ card s
ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n


refine'_2
n ^ ↑Multiset.card s.val ≤ n ^ card s
ι: Type u_1

α: Type ?u.32667

β: Type ?u.32670

M: Type ?u.32673

N: Type u_2

G: Type ?u.32679

k: Type ?u.32682

R: Type ?u.32685

inst✝¹: CommMonoid M

inst✝: OrderedCommMonoid N

f✝, g: ι → N

s✝, t, s: Finset ι

f: ι → N

n: N

h: ∀ (x : ι), x ∈ s → f x ≤ n


refine'_2
n ^ ↑Multiset.card (Multiset.map f s.val) ≤ n ^ card s

Goals accomplished! 🐙
#align finset.prod_le_pow_card
Finset.prod_le_pow_card: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] (s : Finset ι) (f : ι → N) (n : N), (∀ (x : ι), x ∈ s → f x ≤ n) → Finset.prod s f ≤ n ^ card s
Finset.prod_le_pow_card
#align finset.sum_le_card_nsmul
Finset.sum_le_card_nsmul: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] (s : Finset ι) (f : ι → N) (n : N), (∀ (x : ι), x ∈ s → f x ≤ n) → Finset.sum s f ≤ card s • n
Finset.sum_le_card_nsmul
@[to_additive
card_nsmul_le_sum: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] (s : Finset ι) (f : ι → N) (n : N), (∀ (x : ι), x ∈ s → n ≤ f x) → card s • n ≤ Finset.sum s f
card_nsmul_le_sum
] theorem
pow_card_le_prod: ∀ (s : Finset ι) (f : ι → N) (n : N), (∀ (x : ι), x ∈ s → n ≤ f x) → n ^ card s ≤ Finset.prod s f
pow_card_le_prod
(
s: Finset ι
s
:
Finset: Type ?u.56335 → Type ?u.56335
Finset
ι: Type ?u.56291
ι
) (
f: ι → N
f
:
ι: Type ?u.56291
ι
→
N: Type ?u.56303
N
) (
n: N
n
:
N: Type ?u.56303
N
) (
h: ∀ (x : ι), x ∈ s → n ≤ f x
h
: ∀
x: ?m.56345
x
∈
s: Finset ι
s
,
n: N
n
≤
f: ι → N
f
x: ?m.56345
x
) :
n: N
n
^
s: Finset ι
s
.
card: {α : Type ?u.56674} → Finset α → ℕ
card
≤
s: Finset ι
s
.
prod: {β : Type ?u.56679} → {α : Type ?u.56678} → [inst : CommMonoid β] → Finset α → (α → β) → β
prod
f: ι → N
f
:= @
Finset.prod_le_pow_card: ∀ {ι : Type ?u.75259} {N : Type ?u.75260} [inst : OrderedCommMonoid N] (s : Finset ι) (f : ι → N) (n : N), (∀ (x : ι), x ∈ s → f x ≤ n) → Finset.prod s f ≤ n ^ card s
Finset.prod_le_pow_card
_: Type ?u.75259
_
N: Type ?u.56303
N
ᵒᵈ _
_: Finset ?m.75261
_
_: ?m.75261 → Nᵒᵈ
_
_
h: ∀ (x : ι), x ∈ s → n ≤ f x
h
#align finset.pow_card_le_prod
Finset.pow_card_le_prod: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedCommMonoid N] (s : Finset ι) (f : ι → N) (n : N), (∀ (x : ι), x ∈ s → n ≤ f x) → n ^ card s ≤ Finset.prod s f
Finset.pow_card_le_prod
#align finset.card_nsmul_le_sum
Finset.card_nsmul_le_sum: ∀ {ι : Type u_1} {N : Type u_2} [inst : OrderedAddCommMonoid N] (s : Finset ι) (f : ι → N) (n : N), (∀ (x : ι), x ∈ s → n ≤ f x) → card s • n ≤ Finset.sum s f
Finset.card_nsmul_le_sum
theorem
card_biUnion_le_card_mul: ∀ [inst : DecidableEq β] (s : Finset ι) (f : ι → Finset β) (n : ℕ), (∀ (a : ι), a ∈ s → card (f a) ≤ n) → card (Finset.biUnion s f) ≤ card s * n
card_biUnion_le_card_mul
[
DecidableEq: Sort ?u.75423 → Sort (max1?u.75423)
DecidableEq
β: Type ?u.75385
β
] (
s: Finset ι
s
:
Finset: Type ?u.75432 → Type ?u.75432
Finset
ι: Type ?u.75379
ι
) (
f: ι → Finset β
f
:
ι: Type ?u.75379
ι
→
Finset: Type ?u.75437 → Type ?u.75437
Finset
β: Type ?u.75385
β
) (n :
ℕ: Type
ℕ
) (
h: ∀ (a : ι), a ∈ s → card (f a) ≤ n
h
: ∀
a: ?m.75443
a
∈
s: Finset ι
s
, (
f: ι → Finset β
f
a: ?m.75443
a
).
card: {α : Type ?u.75478} → Finset α → ℕ
card
≤ n) : (
s: Finset ι
s
.
biUnion: {α : Type ?u.75494} → {β : Type ?u.75493} → [inst : DecidableEq β] → Finset α → (α → Finset β) → Finset β
biUnion
f: ι → Finset β
f
).
card: {α : Type ?u.75547} → Finset α → ℕ
card
≤
s: Finset ι
s
.
card: {α : Type ?u.75554} → Finset α → ℕ
card
* n :=
card_biUnion_le: ∀ {β : Type ?u.75623} {α : Type ?u.75622} [inst : DecidableEq β] {s : Finset α} {t : α → Finset β}, card (Finset.biUnion s t) ≤ ∑ a in s, card (t a)
card_biUnion_le
.
trans: ∀ {α : Type ?u.75707} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
trans
<|
sum_le_card_nsmul: ∀ {ι : Type ?u.75839} {N : Type ?u.75840} [inst : OrderedAddCommMonoid N] (s : Finset ι) (f : ι → N) (n : N), (∀ (x : ι), x ∈ s → f x ≤ n) → Finset.sum s f ≤ card s • n
sum_le_card_nsmul
_: Finset ?m.75841
_
_: ?m.75841 → ?m.75842
_
_: ?m.75842
_
h: ∀ (a : ι), a ∈ s → card (f a) ≤ n
h
#align finset.card_bUnion_le_card_mul
Finset.card_biUnion_le_card_mul: ∀ {ι : Type u_2} {β : Type u_1} [inst : DecidableEq β] (s : Finset ι) (f : ι → Finset β) (n : ℕ), (∀ (a : ι), a ∈ s → card (f a) ≤ n) → card (Finset.biUnion s f) ≤ card s * n
Finset.card_biUnion_le_card_mul
variable {
ι': Type ?u.78690
ι'
:
Type _: Type (?u.76038+1)
Type _
} [
DecidableEq: Sort ?u.78693 → Sort (max1?u.78693)
DecidableEq
ι': Type ?u.75982
ι'
] -- Porting note: Mathport warning: expanding binder collection (y «expr ∉ » t) @[to_additive
sum_fiberwise_le_sum_of_sum_fiber_nonneg: ∀ {ι : Type u_3} {N : Type u_2} [inst : OrderedAddCommMonoid N] {s : Finset ι} {ι' : Type u_1} [inst_1 : DecidableEq ι'] {t : Finset ι'} {g : ι → ι'} {f : ι → N}, (∀ (y : ι'), ¬y ∈ t → 0 ≤ ∑ x in filter (fun x => g x = y) s, f x) → ∑ y in t, ∑ x in filter (fun x => g x = y) s, f x ≤ ∑ x in s, f x
sum_fiberwise_le_sum_of_sum_fiber_nonneg
] theorem
prod_fiberwise_le_prod_of_one_le_prod_fiber': ∀ {ι : Type u_3} {N : Type u_2} [inst : OrderedCommMonoid N] {s : Finset ι} {ι' : Type u_1} [inst_1 : DecidableEq ι'] {t : Finset ι'} {g : ι → ι'} {f : ι → N}, (∀ (y : ι'), ¬y ∈ t → 1 ≤ ∏ x in filter (fun x => g x = y) s, f x) → ∏ y in t, ∏ x in filter (fun x => g x = y) s, f x ≤ ∏ x in s, f x
prod_fiberwise_le_prod_of_one_le_prod_fiber'
{
t: Finset ι'
t
:
Finset: Type ?u.76050 → Type ?u.76050
Finset
ι': Type ?u.76038
ι'
} {
g: ι → ι'
g
:
ι: Type ?u.75994
ι
→
ι': Type ?u.76038
ι'
} {
f: ι → N
f
:
ι: Type ?u.75994
ι
→
N: Type ?u.76006
N
} (
h: ∀ (y : ι'), ¬y ∈ t → 1 ≤ ∏ x in filter (fun x => g x = y) s, f x
h
: ∀ (
y: ?m.76062
y
) (
_: ¬y ∈ t
_
:
y: ?m.76062
y
∉
t: Finset ι'
t
), (
1: ?m.76087
1
:
N: Type ?u.76006
N
) ≤ ∏
x: ?m.76637
x
in
s: Finset ι
s
.
filter: {α : Type ?u.76593} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter
fun
x: ?m.76602
x
↦
g: ι → ι'
g
x: ?m.76602
x
=
y: ?m.76062
y
,
f: ι → N
f
x: ?m.76637
x
) : (∏
y: ?m.76951
y
in
t: Finset ι'
t
, ∏
x: ?m.77018
x
in
s: Finset ι
s
.
filter: {α : Type ?u.76981} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter
fun
x: ?m.76990
x
↦
g: ι → ι'
g
x: ?m.76990
x
=
y: ?m.76951
y
,
f: ι → N
f
x: ?m.77018
x
) ≤ ∏
x: ?m.77030
x
in
s: Finset ι
s
,
f: ι → N
f
x: ?m.77030
x
:= calc (∏
y: ?m.77056
y
in
t: Finset ι'
t
, ∏
x: ?m.77128
x
in
s: Finset ι
s
.
filter: {α : Type ?u.77086} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter
fun
x: ?m.77095
x
↦
g: ι → ι'
g
x: ?m.77095
x
=
y: ?m.77056
y
,
f: ι → N
f
x: ?m.77128
x
) ≤ ∏
y: ?m.77368
y
in
t: Finset ι'
t
∪
s: Finset ι
s
.
image: {α : Type ?u.77215} → {β : Type ?u.77214} → [inst : DecidableEq β] → (α → β) → Finset α → Finset β
image
g: ι → ι'
g
, ∏
x: ?m.77435
x
in
s: Finset ι
s
.
filter: {α : Type ?u.77398} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter
fun
x: ?m.77407
x
↦
g: ι → ι'
g
x: ?m.77407
x
=
y: ?m.77368
y
,
f: ι → N
f
x: ?m.77435
x
:=
prod_le_prod_of_subset_of_one_le': ∀ {ι : Type ?u.77715} {N : Type ?u.77716} [inst : OrderedCommMonoid N] {f : ι → N} {s t : Finset ι}, s ⊆ t → (∀ (i : ι), i ∈ t → ¬i ∈ s → 1 ≤ f i) → ∏ i in s, f i ≤ ∏ i in t, f i
prod_le_prod_of_subset_of_one_le'
(
subset_union_left: ∀ {α : Type ?u.77756} [inst : DecidableEq α] (s₁ s₂ : Finset α), s₁ ⊆ s₁ ∪ s₂
subset_union_left
_: Finset ?m.77757
_
_: Finset ?m.77757
_
) fun
y: ?m.77868
y
_: ?m.77871
_
↦
h: ∀ (y : ι'), ¬y ∈ t → 1 ≤ ∏ x in filter (fun x => g x = y) s, f x
h
y: ?m.77868
y
_: ?m✝
_
= ∏
x: ?m.77894
x
in
s: Finset ι
s
,
f: ι → N
f
x: ?m.77894
x
:=
prod_fiberwise_of_maps_to: ∀ {β : Type ?u.77900} {α : Type ?u.77899} {γ : Type ?u.77898} [inst : CommMonoid β] [inst_1 : DecidableEq γ] {s : Finset α} {t : Finset γ} {g : α → γ}, (∀ (x : α), x ∈ s → g x ∈ t) → ∀ (f : α → β), ∏ y in t, ∏ x in filter (fun x => g x = y) s, f x = ∏ x in s, f x
prod_fiberwise_of_maps_to
(fun
_: ?m.77910
_
hx: ?m.77913
hx
↦
mem_union: ∀ {α : Type ?u.77915} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t
mem_union
.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2
<|
Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr
<|
mem_image_of_mem: ∀ {α : Type ?u.78018} {β : Type ?u.78019} [inst : DecidableEq β] {s : Finset α} (f : α → β) {a : α}, a ∈ s → f a ∈ image f s
mem_image_of_mem
_: ?m.78020 → ?m.78021
_
hx: ?m.77913
hx
)
_: ?m.77902 → ?m.77901
_
#align finset.prod_fiberwise_le_prod_of_one_le_prod_fiber'
Finset.prod_fiberwise_le_prod_of_one_le_prod_fiber': ∀ {ι : Type u_3} {N : Type u_2} [inst : OrderedCommMonoid N] {s : Finset ι} {ι' : Type u_1} [inst_1 : DecidableEq ι'] {t : Finset ι'} {g : ι → ι'} {f : ι → N}, (∀ (y : ι'), ¬y ∈ t → 1 ≤ ∏ x in filter (fun x => g x = y) s, f x) → ∏ y in t, ∏ x in filter (fun x => g x = y) s, f x ≤ ∏ x in s, f x
Finset.prod_fiberwise_le_prod_of_one_le_prod_fiber'
#align finset.sum_fiberwise_le_sum_of_sum_fiber_nonneg
Finset.sum_fiberwise_le_sum_of_sum_fiber_nonneg: ∀ {ι : Type u_3} {N : Type u_2} [inst : OrderedAddCommMonoid N] {s : Finset ι} {ι' : Type u_1} [inst_1 : DecidableEq ι'] {t : Finset ι'} {g : ι → ι'} {f : ι → N}, (∀ (y : ι'), ¬y ∈ t → 0 ≤ ∑ x in filter (fun x => g x = y) s, f x) → ∑ y in t, ∑ x in filter (fun x => g x = y) s, f x ≤ ∑ x in s, f x
Finset.sum_fiberwise_le_sum_of_sum_fiber_nonneg
-- Porting note: Mathport warning: expanding binder collection (y «expr ∉ » t) @[to_additive
sum_le_sum_fiberwise_of_sum_fiber_nonpos: ∀ {ι : Type u_3} {N : Type u_2} [inst : OrderedAddCommMonoid N] {s : Finset ι} {ι' : Type u_1} [inst_1 : DecidableEq ι'] {t : Finset ι'} {g : ι → ι'} {f : ι → N}, (∀ (y : ι'), ¬y ∈ t → ∑ x in filter (fun x => g x = y) s, f x ≤ 0) → ∑ x in s, f x ≤ ∑ y in t, ∑ x in filter (fun x => g x = y) s, f x
sum_le_sum_fiberwise_of_sum_fiber_nonpos
] theorem
prod_le_prod_fiberwise_of_prod_fiber_le_one': ∀ {t : Finset ι'} {g : ι → ι'} {f : ι → N}, (∀ (y : ι'), ¬y ∈ t → ∏ x in filter (fun x => g x = y) s, f x ≤ 1) → ∏ x in s, f x ≤ ∏ y in t, ∏ x in filter (fun x => g x = y) s, f x
prod_le_prod_fiberwise_of_prod_fiber_le_one'
{
t: Finset ι'
t
:
Finset: Type ?u.78702 → Type ?u.78702
Finset
ι': Type ?u.78690
ι'
} {
g: ι → ι'
g
:
ι: Type ?u.78646
ι
→
ι': Type ?u.78690
ι'
} {
f: ι → N
f
:
ι: Type ?u.78646
ι
→
N: Type ?u.78658
N
} (
h: ∀ (y : ι'), ¬y ∈ t → ∏ x in filter (fun x => g x = y) s, f x ≤ 1
h
: ∀ (
y: ?m.78714
y
) (
_: ¬y ∈ t
_
:
y: ?m.78714
y
∉
t: Finset ι'
t
), (∏
x: ?m.78786
x
in
s: Finset ι
s
.
filter: {α : Type ?u.78742} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter
fun
x: ?m.78751
x
↦
g: ι → ι'
g
x: ?m.78751
x
=
y: ?m.78714
y
,
f: ι → N
f
x: ?m.78786
x
) ≤
1: ?m.78855
1
) : (∏
x: ?m.79615
x
in
s: Finset ι
s
,
f: ι → N
f
x: ?m.79615
x
) ≤ ∏
y: ?m.79625
y
in
t: Finset ι'
t
, ∏
x: ?m.79692
x
in
s: Finset ι
s
.
filter: {α : Type ?u.79655} → (p : α → Prop) → [inst : DecidablePred p] → Finset α → Finset α
filter
fun
x: ?m.79664
x
↦
g: ι → ι'
g
x: ?m.79664
x
=
y: ?m.79625
y
,
f: ι → N
f
x: ?m.79692
x
:= @
prod_fiberwise_le_prod_of_one_le_prod_fiber': ∀ {ι : Type ?u.79712} {N : Type ?u.79711} [inst : OrderedCommMonoid N] {s : Finset ι} {ι' : Type ?u.79710} [inst_1 : DecidableEq ι'] {t : Finset ι'} {g : ι → ι'} {f : ι → N}, (∀ (y : ι'), ¬y ∈ t → 1 ≤ ∏ x in filter (fun x => g x = y) s, f x) → ∏ y in t, ∏ x in filter (fun x => g x = y) s, f x ≤ ∏ x in s, f x
prod_fiberwise_le_prod_of_one_le_prod_fiber'
_: Type ?u.79712
_
N: Type ?u.78658
N
ᵒᵈ _
_: Finset ?m.79713
_
_: Type ?u.79710
_
_
_: Finset ?m.79717
_
_: ?m.79713 → ?m.79717
_
_: ?m.79713 → Nᵒᵈ
_
h: ∀ (y : ι'), ¬y ∈ t → ∏ x in filter (fun x => g x = y) s, f x ≤ 1
h
#align finset.prod_le_prod_fiberwise_of_prod_fiber_le_one'
Finset.prod_le_prod_fiberwise_of_prod_fiber_le_one': ∀ {ι : Type u_3} {N : Type u_2} [inst : OrderedCommMonoid N] {s : Finset ι} {ι' : Type u_1} [inst_1 : DecidableEq ι'] {t : Finset ι'} {g : ι → ι'} {f :