closedBall_one_div — Mathlib

English

If s is compact and δ ≥ 0, then closedBall(1, δ) / s equals the δ-thickening of s⁻¹; i.e. closedBall(1, δ) / s = cthickening(δ, s⁻¹).

Русский

Если s компактно и δ ≥ 0, то closedBall(1, δ) / s = cthickening(δ, s⁻¹).

LaTeX

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

Lean4

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

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