mul_le_dist

Mathlib.Topology.MetricSpace.Antilipschitz

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

English

In the distance setting, K⁻¹ dist(x,y) ≤ dist(f x, f y).

Русский

В расстояниях: K⁻¹ dist(x,y) ≤ dist(f x, f y).

LaTeX

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

Lean4

theorem mul_le_dist (hf : AntilipschitzWith K f) (x y : α) : (K⁻¹ * dist x y : ℝ) ≤ dist (f x) (f y) :=
  mod_cast hf.mul_le_nndist x y

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

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

Разделы

Аффилиация

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