enorm_sum_le — Mathlib

English

If for each b in s we have dist(f(b), a(b)) ≤ d(b), then dist(∏ f(b), ∏ a(b)) ≤ ∑ d(b).

Русский

Если для каждого b в s верно dist(f(b), a(b)) ≤ d(b), то dist(∏ f(b), ∏ a(b)) ≤ ∑ d(b).

LaTeX

$$$$\operatorname{dist}\Big(\prod_{b\in s} f(b), \prod_{b\in s} a(b)\Big) \le \sum_{b\in s} d(b).$$$$

Lean4

@[bound]
theorem enorm_sum_le (s : Finset ι) (f : ι → ε) : ‖∑ i ∈ s, f i‖ₑ ≤ ∑ i ∈ s, ‖f i‖ₑ :=
  s.le_sum_of_subadditive enorm enorm_zero enorm_add_le f

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