dist_div_div_le_of_le — Mathlib

English

If dist(a1,b1) ≤ r1 and dist(a2,b2) ≤ r2, then dist(a1/a2, b1/b2) ≤ r1 + r2.

Русский

Если dist(a1,b1) ≤ r1 и dist(a2,b2) ≤ r2, то dist(a1/a2, b1/b2) ≤ r1 + r2.

LaTeX

$$$\left( dist(a_1,b_1) \le r_1 \right) \land \left( dist(a_2,b_2) \le r_2 \right) \Rightarrow dist\left(\dfrac{a_1}{a_2}, \dfrac{b_1}{b_2}\right) \le r_1 + r_2.$$$

Lean4

@[to_additive]
theorem dist_div_div_le_of_le (h₁ : dist a₁ b₁ ≤ r₁) (h₂ : dist a₂ b₂ ≤ r₂) : dist (a₁ / a₂) (b₁ / b₂) ≤ r₁ + r₂ :=
  (dist_div_div_le a₁ a₂ b₁ b₂).trans <| add_le_add h₁ h₂

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