singleton_div_closedBall — Mathlib

English

Division by a closed ball distributes over the singleton: {x} / closedBall(y, δ) = closedBall(x/y, δ).

Русский

Деление единичного множества на замкнутый шар distributes: {x} / closedBall(y, δ) = closedBall(x/y, δ).

LaTeX

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

Lean4

@[to_additive (attr := simp 1100)]
theorem singleton_div_closedBall : { x } / closedBall y δ = closedBall (x / y) δ := by
  simp_rw [div_eq_mul_inv, inv_closedBall, singleton_mul_closedBall]

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