max_const — Mathlib

English

If f is locally Lipschitz, then the function x ↦ max(f(x), a) is locally Lipschitz for any real a.

Русский

Если f локально липшицево, то функция x ↦ max(f(x), a) локально липшицева для любого числа a.

LaTeX

$$$(\\text{LocallyLipschitz} f) \\Rightarrow \\forall a \\in \\mathbb{R}, \\text{LocallyLipschitz}\\big( x \\mapsto \\max(f(x), a)\\big).$$$

Lean4

theorem max_const (hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun x => max (f x) a :=
  hf.max (LocallyLipschitz.const a)

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