dist_prod_prod_le_of_le — Mathlib

English

If for every b in s, dist(f(b), a(b)) ≤ d(b), then the distance between the products is ≤ the sum of 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

@[to_additive]
theorem dist_prod_prod_le_of_le (s : Finset ι) {f a : ι → E} {d : ι → ℝ} (h : ∀ b ∈ s, dist (f b) (a b) ≤ d b) :
    dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, d b :=
  by
  simp only [dist_eq_norm_div, ← Finset.prod_div_distrib] at *
  exact norm_prod_le_of_le s h

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