const_max — Mathlib

English

If f is locally Lipschitz, then x ↦ max(a, f(x)) is locally Lipschitz for any a ∈ ℝ.

Русский

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

LaTeX

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

Lean4

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

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