const_max

Mathlib.Topology.MetricSpace.Lipschitz

URI: https://scilib.ai/kg/mathlib#LipschitzWith.const_max

English

For real a ≤ b, the projection onto the closed interval [a,b] is 1-Lipschitz.

Русский

Проекция на замкнутый интервал [a,b] является 1- Lipschitz.

LaTeX

$$$\\text{LipschitzWith}(1,\\, \\operatorname{Set.projIcc}~a~b~h)$$$

Lean4

theorem const_max (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => max a (f x) := by
  simpa only [max_comm] using hf.max_const a

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

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

Разделы

Аффилиация

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