ι : 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)
refine' le_trans (Multiset.le_prod_of_submultiplicative f h_one h_mul _) _
ι : 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 (Multiset.map (fun i => g i) s.val)) ≤ ∏ i in s, f (g i)
rw [Multiset.map_map]
no goals
ι : 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)
rfl