closedBall_one_mul — Mathlib

English

If s is compact and δ ≥ 0, then closedBall(1, δ) · s equals cthickening(δ, s).

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem closedBall_one_mul (hs : IsCompact s) (hδ : 0 ≤ δ) : closedBall 1 δ * s = cthickening δ s := by
  rw [mul_comm, hs.mul_closedBall_one hδ]

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