mapsTo_closedBall — Mathlib

English

Dilation maps closed balls to closed balls with radius scaled by ratio f.

Русский

Дилатация отображает замкнутые шары в замкнутые шары, радиус масштабируется ratio f.

LaTeX

$$$\\text{MapsTo}(f, \\text{Metric.closedBall}(x,r')) \\; \\text{to} \\; \\text{Metric.closedBall}(f(x), \\operatorname{ratio}(f) \\cdot r')$$$

Lean4

/-- A dilation maps closed balls to closed balls and scales the radius by `ratio f`. -/
theorem mapsTo_closedBall (x : α) (r' : ℝ) :
    MapsTo (f : α → β) (Metric.closedBall x r') (Metric.closedBall (f x) (ratio f * r')) := fun y hy =>
  (dist_eq f y x).trans_le <| mul_le_mul_of_nonneg_left hy (NNReal.coe_nonneg _)

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