max — Mathlib

English

If f is K-Lipschitz and a is a real constant, then x ↦ max(f(x), a) is Lipschitz with the same constant K.

Русский

Если f липшицев с константой K, и a — константа, то max(f(x), a) липшиев с константой K.

LaTeX

$$$\\operatorname{LipschitzWith}(K_f, f) \\Rightarrow \\operatorname{LipschitzWith}(K_f, \\lambda x. \\max(f(x), a))$$$

Lean4

protected theorem max (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
    LipschitzWith (max Kf Kg) fun x => max (f x) (g x) := by
  simpa only [(· ∘ ·), one_mul] using lipschitzWith_max.comp (hf.prodMk hg)

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