of_nnnorm_bounded — Mathlib

English

If every ‖f i‖₊ ≤ g i for a summable NNReal g, then f is summable.

Русский

Если для всех i выполняется ‖f i‖₊ ≤ g i с суммируемым NNReal g, то f суммируема.

LaTeX

$$$\\text{Summable } g \\Rightarrow (\\forall i, \\|f(i)\\|_+ ≤ g(i) \\Rightarrow \\text{Summable } f)$$$

Lean4

theorem of_nnnorm_bounded {f : ι → E} {g : ι → ℝ≥0} (hg : Summable g) (h : ∀ i, ‖f i‖₊ ≤ g i) : Summable f :=
  .of_norm_bounded (NNReal.summable_coe.2 hg) h

Похожие утверждения