mul_le_nndist

Mathlib.Topology.MetricSpace.Antilipschitz

URI: https://scilib.ai/kg/mathlib#AntilipschitzWith.mul_le_nndist

← MathLib Explorer

English

If f is AntilipschitzWith K, then K⁻¹ · nndist(x,y) ≤ nndist(f x, f y).

Русский

Если f антип Lipschitz с константой K, то K⁻¹ · nndist(x,y) ≤ nndist(f x, f y).

LaTeX

$$$K^{-1} \\cdot nndist(x,y) \\le nndist(f x, f y)$$$

Lean4

theorem mul_le_nndist (hf : AntilipschitzWith K f) (x y : α) : K⁻¹ * nndist x y ≤ nndist (f x) (f y) := by
  simpa only [div_eq_inv_mul] using NNReal.div_le_of_le_mul' (hf.le_mul_nndist x y)

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

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

Разделы

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

Аффилиация

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