English
Dilation maps spheres to spheres and scales the radius by ratio f.
Русский
Дилатация отображает сферы в сферы и масштабирует радиус на ratio f.
LaTeX
$$$\\text{MapsTo}(f, \\text{Metric.sphere}(x,r')) \\; \\text{to} \\; \\text{Metric.sphere}(f(x), \\operatorname{ratio}(f) \\cdot r')$$$
Lean4
/-- A dilation maps spheres to spheres and scales the radius by `ratio f`. -/
theorem mapsTo_sphere (x : α) (r' : ℝ) : MapsTo (f : α → β) (Metric.sphere x r') (Metric.sphere (f x) (ratio f * r')) :=
fun y hy => Metric.mem_sphere.mp hy ▸ dist_eq f y x