div_closedBall — Mathlib

English

For compact s and δ ≥ 0, s / closedBall(1, δ) = cthickening(δ, s⁻¹).

Русский

Для компактного s и δ ≥ 0 верно: s / closedBall(1, δ) = cthickening(δ, s⁻¹).

LaTeX

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

Lean4

@[to_additive]
theorem div_closedBall (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : s / closedBall x δ = x⁻¹ • cthickening δ s := by
  simp [div_eq_mul_inv, hs.mul_closedBall hδ]

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