mapsTo_emetric_closedBall — Mathlib

English

A Lipschitz function maps a closed ball to a ball with radius scaled by K.

Русский

Липшицева функция отображает закрытый шар в шар с радиусом, умноженным на K.

LaTeX

$$$MapsTo\ f\ (closedBall\ x\ r)\ (closedBall\ (f(x))\ (K \cdot r))$$$

Lean4

theorem mapsTo_emetric_closedBall (h : LipschitzWith K f) (x : α) (r : ℝ≥0∞) :
    MapsTo f (closedBall x r) (closedBall (f x) (K * r)) := fun _y hy => h.edist_le_mul_of_le hy

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