dist_div_div_le — Mathlib

English

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

Русский

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

LaTeX

$$$\forall a_1,a_2,b_1,b_2,\ dist\left(\dfrac{a_1}{a_2}, \dfrac{b_1}{b_2}\right) \le dist(a_1,b_1) + dist(a_2,b_2).$$$

Lean4

@[to_additive]
theorem dist_div_div_le (a₁ a₂ b₁ b₂ : E) : dist (a₁ / a₂) (b₁ / b₂) ≤ dist a₁ b₁ + dist a₂ b₂ := by
  simpa only [div_eq_mul_inv, dist_inv_inv] using dist_mul_mul_le a₁ a₂⁻¹ b₁ b₂⁻¹

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