closedBall_one_div_singleton — Mathlib

English

The closed unit ball divided by a singleton equals the closed ball around the inverse: closedBall(1, δ) / {x} = closedBall(x^{-1}, δ).

Русский

Деление замкнутого шарa единицы на один элемент равно замкнутому шару вокруг x^{-1}: closedBall(1, δ) / {x} = closedBall(x^{-1}, δ).

LaTeX

$$$${\overline{B}}(1,\delta) / \{x\} = \overline{B}(x^{-1},\delta)$$$$

Lean4

@[to_additive]
theorem closedBall_one_div_singleton : closedBall 1 δ / { x } = closedBall x⁻¹ δ := by simp

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