mapsTo_closedBall — Mathlib

English

A Lipschitz function maps a closed ball into a larger closed ball with radius scaled by the Lipschitz constant.

Русский

Функция с Lip-константой отображает замкнутый шар в другой замкнутый шар радиуса, умноженного на константу липшицевости.

LaTeX

$$$\forall x,r,\ f(\overline{B}(x,r)) \subseteq \overline{B}(f(x), K r)$$$

Lean4

theorem mapsTo_closedBall (hf : LipschitzWith K f) (x : α) (r : ℝ) :
    MapsTo f (Metric.closedBall x r) (Metric.closedBall (f x) (K * r)) := fun _y hy => hf.dist_le_mul_of_le hy

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