abs_dist_sub_le_dist_mul_mul — Mathlib

English

For a1,a2,b1,b2 in a seminormed commutative group, |dist(a1,b1) - dist(a2,b2)| ≤ dist(a1 a2, b1 b2).

Русский

Для элементов a1,a2,b1,b2 в нормированной коммутативной группе выполняется |dist(a1,b1) - dist(a2,b2)| ≤ dist(a1 a2, b1 b2).

LaTeX

$$$\left| \mathrm{dist}(a_1,b_1) - \mathrm{dist}(a_2,b_2) \right| \le \mathrm{dist}(a_1 a_2, b_1 b_2).$$$

Lean4

@[to_additive]
theorem abs_dist_sub_le_dist_mul_mul (a₁ a₂ b₁ b₂ : E) : |dist a₁ b₁ - dist a₂ b₂| ≤ dist (a₁ * a₂) (b₁ * b₂) := by
  simpa only [dist_mul_left, dist_mul_right, dist_comm b₂] using abs_dist_sub_le (a₁ * a₂) (b₁ * b₂) (b₁ * a₂)

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