English
If s does not contain zero, then the product s · sphere(0,r) equals the preimage under the norm map of the radii obtained by scaling s.
Русский
Если s не содержит нуль, то s · сфера(0,r) равняется предобразованию по норме от множества значений ‖c‖·r, где c∈s.
LaTeX
$$$s \cdot \mathrm{sphere}(0,r) = \|\cdot\|^{-1}'(\{\|c\| \cdot r: c \in s\}).$$$
Lean4
theorem set_smul_sphere_zero {s : Set 𝕜} (hs : 0 ∉ s) (r : ℝ) : s • sphere (0 : E) r = (‖·‖) ⁻¹' ((‖·‖ * r) '' s) :=
calc
s • sphere (0 : E) r = ⋃ c ∈ s, c • sphere (0 : E) r := iUnion_smul_left_image.symm
_ = ⋃ c ∈ s, sphere (0 : E) (‖c‖ * r) :=
(iUnion₂_congr fun c hc ↦ by rw [smul_sphere' (ne_of_mem_of_not_mem hc hs), smul_zero])
_ = (‖·‖) ⁻¹' ((‖·‖ * r) '' s) := by ext; simp [eq_comm]
