singleton_div_ball — Mathlib

English

For a fixed x, the left division by the ball around y preserves radius: {x} / ball(y, δ) = ball(x/y, δ).

Русский

Пусть x фиксирован. Левое деление на шар вокруг y сохраняет радиус: {x} / ball(y, δ) = ball(x/y, δ).

LaTeX

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

Lean4

@[to_additive]
theorem singleton_div_ball : { x } / ball y δ = ball (x / y) δ := by
  simp_rw [div_eq_mul_inv, inv_ball, singleton_mul_ball]

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