English
Let s be a finite index set and E a seminormed commutative group. For any two families f and a of elements of E indexed by s, the distance between the products ∏_{b∈s} f(b) and ∏_{b∈s} a(b) is bounded by the sum of the distances of the corresponding factors:
Русский
Пусть s — конечное множество индексов, E — полугруппа с нормой. Для любых функций f, a : s → E выполняется неравенство расстояния между произведениями в сторону суммы расстояний попарно:
LaTeX
$$$\displaystyle \text{Let }s\text{ be a finite set of indices }f,a: s\to E:\\[ \\qquad d\Big(\prod_{b\in s} f(b),\\prod_{b\in s} a(b)\Big) \le \sum_{b\in s} d(f(b), a(b)).$$$
Lean4
@[to_additive]
theorem dist_prod_prod_le (s : Finset ι) (f a : ι → E) :
dist (∏ b ∈ s, f b) (∏ b ∈ s, a b) ≤ ∑ b ∈ s, dist (f b) (a b) :=
dist_prod_prod_le_of_le s fun _ _ => le_rfl
