α : Type u_1
β : Type ?u.206222
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
hs : Finset.Nonempty s
f g : α → ℝ≥0∞
Hle : ∀ (i : α), i ∈ s → g i < f i
⊢ ∑ i in s, g i < ∑ i in s, f i
α : Type u_1
β : Type ?u.206222
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
hs : Finset.Nonempty s
f g : α → ℝ≥0∞
Hle : ∑ i in s, f i ≤ ∑ i in s, g i
⊢ ∃ i, i ∈ s ∧ f i ≤ g i
contrapose! Hle
no goals
α : Type u_1
β : Type ?u.206222
a b c d : ℝ≥0∞
r p q : ℝ≥0
s : Finset α
hs : Finset.Nonempty s
f g : α → ℝ≥0∞
Hle : ∀ (i : α), i ∈ s → g i < f i
⊢ ∑ i in s, g i < ∑ i in s, f i
apply ENNReal.sum_lt_sum_of_nonempty hs Hle