English
For f : β → ℝ≥0, the infinite sum of ENNReal of its nonnegative real lift is not ∞ if and only if f is summable.
Русский
Для f: β → ℝ≥0, бесконечная сумма ENNReal от поднятия значений неравна ∞ тогда и только тогда, когда f суммируема.
LaTeX
$$$(\\sum' b, (f b : \\mathbb{R}_{\\ge 0}^{\\infty})) \\neq \\infty \\iff \\text{Summable } f$.$$
Lean4
@[macro Mathlib.Tactic.GCongr.tacticGcongr_discharger]
public meta def
_aux_Mathlib_Topology_Instances_ENNReal_Lemmas___macroRules_Mathlib_Tactic_GCongr_tacticGcongr_discharger_1 :
Macro✝ := fun
| `(tactic| gcongr_discharger) => `(tactic| apply ENNReal.summable)
| _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝
