lipschitzWith_max — Mathlib

English

If f and g are Lipschitz with constants Kf and Kg, then x ↦ max(f(x), g(x)) is Lipschitz with constant max(Kf, Kg).

Русский

Если f и g липшицевы с константами Kf и Kg, то F(x)=max(f(x),g(x)) липшицев с константой max(Kf,Kg).

LaTeX

$$$\\operatorname{LipschitzWith}(\\max(K_f,K_g),\\, \\lambda x. \\max(f(x),g(x)))$$$

Lean4

theorem _root_.lipschitzWith_max : LipschitzWith 1 fun p : ℝ × ℝ => max p.1 p.2 :=
  LipschitzWith.of_le_add fun _ _ => sub_le_iff_le_add'.1 <| (le_abs_self _).trans (abs_max_sub_max_le_max _ _ _ _)

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