edist_le_mul_of_le

Mathlib.Topology.EMetricSpace.Lipschitz

URI: https://scilib.ai/kg/mathlib#LipschitzWith.edist_le_mul_of_le

English

If edist(x,y) ≤ r, then edist(f x, f y) ≤ K · r.

Русский

Если edist(x,y) ≤ r, то edist(f x, f y) ≤ K · r.

LaTeX

$$$edist(x,y) \le r \Rightarrow edist(f(x),f(y)) \le K \cdot r$$$

Lean4

theorem edist_le_mul_of_le (h : LipschitzWith K f) (hr : edist x y ≤ r) : edist (f x) (f y) ≤ K * r :=
  (h x y).trans <| mul_right_mono hr

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru