mapsTo_sphere — Mathlib

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

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