dist_mul_mul_le — Mathlib

English

For a1,a2,b1,b2 in a seminormed commutative group, the distance between products is bounded by the sum of the componentwise distances: dist(a1 a2, b1 b2) ≤ dist(a1,b1) + dist(a2,b2).

Русский

В полугруппе с нормой выполняется неравенство: dist(a1 a2, b1 b2) ≤ dist(a1,b1) + dist(a2,b2).

LaTeX

$$$\forall a_1,a_2,b_1,b_2,\ dist(a_1 a_2, b_1 b_2) \le dist(a_1,b_1) + dist(a_2,b_2).$$$

Lean4

@[to_additive]
theorem dist_mul_mul_le (a₁ a₂ b₁ b₂ : E) : dist (a₁ * a₂) (b₁ * b₂) ≤ dist a₁ b₁ + dist a₂ b₂ := by
  simpa only [dist_mul_left, dist_mul_right] using dist_triangle (a₁ * a₂) (b₁ * a₂) (b₁ * b₂)

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