max — Mathlib

English

If f and g are locally Lipschitz, then the pointwise maximum h(x) = max(f(x), g(x)) is locally Lipschitz.

Русский

Если f и g — локально липшицевыe функции, то поштучный максимум h(x) = max(f(x), g(x)) также локально липшицево.

LaTeX

$$$(\\text{LocallyLipschitz} f) \\land (\\text{LocallyLipschitz} g) \\Rightarrow \\text{LocallyLipschitz}\\big( x \\mapsto \\max\\big(f(x),\\; g(x)\\big)\\big).$$$

Lean4

/-- The maximum of locally Lipschitz functions is locally Lipschitz. -/
protected theorem max (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :
    LocallyLipschitz (fun x => max (f x) (g x)) :=
  lipschitzWith_max.locallyLipschitz.comp (hf.prodMk hg)

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