closedBall_div_singleton — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp 1100)]
theorem closedBall_div_singleton : closedBall x δ / { y } = closedBall (x / y) δ := by simp [div_eq_mul_inv]

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