div_closedBall_one — Mathlib

English

If s is compact and δ ≥ 0, then s · closedBall(1, δ) equals the thickening of s by δ; i.e. s * closedBall(1, δ) = cthickening(δ, s).

Русский

Если s компактно и δ ≥ 0, то s · closedBall(1, δ) равно утолщению s на δ.

LaTeX

$$$s \cdot \operatorname{closedBall}(1, \delta) = \operatorname{cthickening}(\delta, s)$$$

Lean4

@[to_additive]
theorem div_closedBall_one (hs : IsCompact s) (hδ : 0 ≤ δ) : s / closedBall 1 δ = cthickening δ s := by
  simp [div_eq_mul_inv, hs.mul_closedBall_one hδ]

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