Theorem: Real.summable_of_le (Carleson/Theorem1_1/Approximation.lean)

State before:
β : Type
f g : β → ℝ
hgpos : 0 ≤ g
hgf : ∀ (b : β), g b ≤ f b
summablef : Summable f
⊢ Summable g
Tactic:
exact Summable.of_nonneg_of_le hgpos hgf summablef
State after:
no goals