mul_ball_one — Mathlib

English

For any set s, s * ball 1 δ equals the thickening of s by δ: s * ball(1, δ) = thickening(δ, s).

Русский

Для множества s произведение с шаром единицы δ даёт утолщение δ соседствующего множества: s * ball(1, δ) = thickening(δ, s).

LaTeX

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

Lean4

@[to_additive]
theorem mul_ball_one : s * ball 1 δ = thickening δ s :=
  by
  rw [thickening_eq_biUnion_ball]
  convert iUnion₂_mul (fun x (_ : x ∈ s) => { x }) (ball (1 : E) δ)
  · exact s.biUnion_of_singleton.symm
  ext x
  simp_rw [singleton_mul_ball, mul_one]

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