English
In the real normed space setting, for a ≥ 0 and r > 0, the smoothed interval Ioo(a,b) scales the sphere into the corresponding annulus.
Русский
В вещественном нормированном пространстве при a ≥ 0 и r > 0, умножение множества Ioo(a,b) на sphere масштабирует сферу в соответствующую облицовку.
LaTeX
$$$Ioo(a,b) \cdot \mathrm{sphere}(0,r) = \mathrm{ball}(0, br) \setminus \mathrm{closedBall}(0, ar).$$$
Lean4
theorem Ioo_smul_sphere_zero {a b r : ℝ} (ha : 0 ≤ a) (hr : 0 < r) :
Ioo a b • sphere (0 : E) r = ball 0 (b * r) \ closedBall 0 (a * r) :=
by
have : EqOn (‖·‖) id (Ioo a b) := fun x hx ↦ abs_of_pos (ha.trans_lt hx.1)
rw [set_smul_sphere_zero (by simp [ha.not_gt]), ← image_image (· * r), this.image_eq, image_id,
image_mul_right_Ioo _ _ hr]
ext x;
simp [and_comm]
-- This is also true for `ℚ`-normed spaces
