Theorems · Theorem · functional analysis

dist_prod_prod_le_of_le

∀ {ι : Type u_3} {E : Type u_5} [inst : SeminormedCommGroup E] (s : Finset ι) {f a : ι → E} {d : ι → ℝ},
  (∀ b ∈ s, dist (f b) (a b) ≤ d b) → dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, d b

Defined in

Mathlib.Analysis.Normed.Group.Basic

Cited by

1 results in Mathlib

Foundations

Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedCommGroup