α : Type ?u.310040
β : Type u_1
γ : Type ?u.310046
f g : β → ℝ≥0
r : ℝ≥0
hgf : ∀ (b : β), g b ≤ f b
hfr : HasSum f r
b : β
⊢ ↑(g b) ≤ ↑(f b)
α : Type ?u.310040
β : Type u_1
γ : Type ?u.310046
f g : β → ℝ≥0
r : ℝ≥0
hgf : ∀ (b : β), g b ≤ f b
hfr : HasSum f r
⊢ (∑' (b : β), ↑(g b)) ≤ ↑r
refine hasSum_le (fun b => ?_) ENNReal.summable.hasSum (ENNReal.hasSum_coe.2 hfr)
no goals
α : Type ?u.310040
β : Type u_1
γ : Type ?u.310046
f g : β → ℝ≥0
r : ℝ≥0
hgf : ∀ (b : β), g b ≤ f b
hfr : HasSum f r
b : β
⊢ ↑(g b) ≤ ↑(f b)
exact ENNReal.coe_le_coe.2 (hgf _)