min — Mathlib

English

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

Русский

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

LaTeX

$$$\\operatorname{LipschitzWith}(K, f) \\Rightarrow \\operatorname{LipschitzWith}(K, \\lambda x. \\min(a, f(x)))$$$

Lean4

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

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