mul_closedBall_one — Mathlib

English

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

Русский

Пусть s компактно, δ ≥ 0. Тогда s · closedBall(1, δ) = cthickening(δ, s).

LaTeX

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

Lean4

@[to_additive]
theorem mul_closedBall_one (hs : IsCompact s) (hδ : 0 ≤ δ) : s * closedBall (1 : E) δ = cthickening δ s :=
  by
  rw [hs.cthickening_eq_biUnion_closedBall hδ]
  ext x
  simp only [mem_mul, dist_eq_norm_div, exists_prop, mem_iUnion, mem_closedBall, ← eq_div_iff_mul_eq'', div_one,
    exists_eq_right]

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