norm_le_of_bounded — Mathlib

English

If HasSum f a and HasSum g b and ‖f i‖ ≤ g i for all i, then ‖a‖ ≤ b.

Русский

Если HasSum f a и HasSum g b и ‖f(i)‖ ≤ g(i) для всех i, то ‖a‖ ≤ b.

LaTeX

$$$\\text{HasSum } f a \\land \\text{HasSum } g b \\land (\\forall i, \\|f(i)\\| \\le g(i)) \\Rightarrow \\|a\\| \\le b$$$

Lean4

theorem norm_le_of_bounded {f : ι → E} {g : ι → ℝ} {a : E} {b : ℝ} (hf : HasSum f a) (hg : HasSum g b)
    (h : ∀ i, ‖f i‖ ≤ g i) : ‖a‖ ≤ b := by
  exact le_of_tendsto_of_tendsto' hf.norm hg fun _s ↦ norm_sum_le_of_le _ fun i _hi ↦ h i

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