const

Mathlib.Topology.EMetricSpace.Lipschitz

URI: https://scilib.ai/kg/mathlib#LocallyLipschitz.const

← MathLib Explorer

English

Constant functions are locally Lipschitz.

Русский

Постоянные отображения локально липшицевы.

LaTeX

$$$\\forall b,\\ LocallyLipschitz(\\lambda x. b)$$$

Lean4

/-- Constant functions are locally Lipschitz. -/
protected theorem const (b : β) : LocallyLipschitz (fun _ : α ↦ b) :=
  (LipschitzWith.const b).locallyLipschitz

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

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

Разделы

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

Аффилиация

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