ball_div_singleton — Mathlib

English

Division by a singleton distributes over balls: ball δ / {y} = ball(δ) divided by y, i.e., ball(x/y, δ).

Русский

Деление на единичное множество распределяется по шарам: ball(x, δ) / {y} = ball(x/y, δ).

LaTeX

$$$$B(x,\delta) / \{y\} = B\left(\tfrac{x}{y},\delta\right)$$$$

Lean4

@[to_additive]
theorem ball_div_singleton : ball x δ / { y } = ball (x / y) δ := by
  simp_rw [div_eq_mul_inv, inv_singleton, ball_mul_singleton]

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