closedBall_mul — Mathlib

English

For compact s and δ ≥ 0, closedBall(x, δ) · s = x · cthickening(δ, s).

Русский

Для компактного s и δ ≥ 0 верно closedBall(x, δ) · s = x · cthickening(δ, s).

LaTeX

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

Lean4

@[to_additive]
theorem closedBall_mul (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : closedBall x δ * s = x • cthickening δ s := by
  rw [mul_comm, hs.mul_closedBall hδ]

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