const'

Mathlib.Topology.EMetricSpace.Lipschitz

URI: https://scilib.ai/kg/mathlib#LipschitzWith.const'

English

Constant functions are Lipschitz with any constant K.

Русский

Функции-константы являются липшицевыми с любой константой K.

LaTeX

$$$\text{const}'(b):\;\text{LipschitzWith}(K,\lambda x. b)$ for any K, b.$$

Lean4

protected theorem const' (b : β) {K : ℝ≥0} : LipschitzWith K fun _ : α => b := fun x y => by
  simp only [edist_self, zero_le]

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

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

Разделы

Аффилиация

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