English
Let E be a seminormed commutative group. For all a1, a2, b1, b2 in E, the nonnegative distance between products satisfies nndist(a1 a2, b1 b2) ≤ nndist(a1, b1) + nndist(a2, b2).
Русский
Пусть E — полугруппа с нормой (коммутативная). Для любых a1, a2, b1, b2 ∈ E выполнено неотрицательное расстояние между произведениями ≤ сумма расстояний между соответствующими множителями: nndist(a1 a2, b1 b2) ≤ nndist(a1, b1) + nndist(a2, b2).
LaTeX
$$$\\forall a_1,a_2,b_1,b_2\\in E:\\; \\mathrm{nndist}(a_1 a_2, b_1 b_2) \\le \\mathrm{nndist}(a_1,b_1) + \\mathrm{nndist}(a_2,b_2).$$$
Lean4
@[to_additive]
theorem nndist_mul_mul_le (a₁ a₂ b₁ b₂ : E) : nndist (a₁ * a₂) (b₁ * b₂) ≤ nndist a₁ b₁ + nndist a₂ b₂ :=
NNReal.coe_le_coe.1 <| dist_mul_mul_le a₁ a₂ b₁ b₂
