k

Mathlib.Topology.MetricSpace.Antilipschitz

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

← MathLib Explorer

English

In the edistance setting, K⁻¹ · edist(x,y) ≤ edist(f x, f y).

Русский

В eddistance: K⁻¹ · edist(x,y) ≤ edist(f x, f y).

LaTeX

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

Lean4

/-- Extract the constant from `hf : AntilipschitzWith K f`. This is useful, e.g.,
if `K` is given by a long formula, and we want to reuse this value. -/
@[nolint unusedArguments]
protected def k (_hf : AntilipschitzWith K f) : ℝ≥0 :=
  K

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

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

Разделы

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

Аффилиация

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