edist_lt_mul_of_lt

Mathlib.Topology.EMetricSpace.Lipschitz

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

← MathLib Explorer

English

If K ≠ 0 and edist(x,y) < r, then edist(f x, f y) < K · r.

Русский

Если K ≠ 0 и edist(x,y) < r, тогда edist(f x, f y) < K · r.

LaTeX

$$$K \neq 0 \land edist(x,y) < r \Rightarrow edist(f(x),f(y)) < K \cdot r$$$

Lean4

theorem edist_lt_mul_of_lt (h : LipschitzWith K f) (hK : K ≠ 0) (hr : edist x y < r) : edist (f x) (f y) < K * r :=
  (h x y).trans_lt <| (ENNReal.mul_lt_mul_left (ENNReal.coe_ne_zero.2 hK) ENNReal.coe_ne_top).2 hr

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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