ball_div_one — Mathlib

English

Ball divided by a singleton corresponds to thickening by the inverse set: ball 1 δ / s = thickening(δ, s^{-1}).

Русский

Шар делится на единичное множество как утолщение на обратное множество: ball(1, δ) / s = thickening(δ, s^{-1}).

LaTeX

$$$$B(1,\delta) / s = \operatorname{thickening}(\delta, s^{-1})$$$$

Lean4

@[to_additive]
theorem ball_div_one : ball 1 δ / s = thickening δ s⁻¹ := by simp [div_eq_mul_inv, ball_mul_one]

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