ι : Type u_1
α : Type u_2
β : Type ?u.17209
inst✝ : LinearOrderedRing α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : MonovaryOn f g ↑s
⊢ (∑ i in s, f i) * ∑ i in s, g i ≤ card s • ∑ i in s, f i * g i
ι : Type u_1
α : Type u_2
β : Type ?u.17209
inst✝ : LinearOrderedRing α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : MonovaryOn f g ↑s
⊢ (∑ i in s, f i) * ∑ i in s, g i ≤ ↑(card s) * ∑ i in s, f i * g i
rw [← nsmul_eq_mul]
no goals
ι : Type u_1
α : Type u_2
β : Type ?u.17209
inst✝ : LinearOrderedRing α
s : Finset ι
σ : Perm ι
f g : ι → α
hfg : MonovaryOn f g ↑s
⊢ (∑ i in s, f i) * ∑ i in s, g i ≤ card s • ∑ i in s, f i * g i
exact hfg.sum_smul_sum_le_card_smul_sum