dist_mul_mul_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(a_1 a_2, b_1 b_2) \le r_1 + r_2.$$$

Lean4

@[to_additive]
theorem dist_mul_mul_le_of_le (h₁ : dist a₁ b₁ ≤ r₁) (h₂ : dist a₂ b₂ ≤ r₂) : dist (a₁ * a₂) (b₁ * b₂) ≤ r₁ + r₂ :=
  (dist_mul_mul_le a₁ a₂ b₁ b₂).trans <| add_le_add h₁ h₂

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