mul_closedBall — Mathlib

English

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

Русский

Для произвольной x и компактного 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 mul_closedBall (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) : s * closedBall x δ = x • cthickening δ s := by
  rw [← smul_closedBall_one, mul_smul_comm, hs.mul_closedBall_one hδ]

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