lipschitzWith_min — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem _root_.lipschitzWith_min : LipschitzWith 1 fun p : ℝ × ℝ => min p.1 p.2 :=
  LipschitzWith.of_le_add fun _ _ => sub_le_iff_le_add'.1 <| (le_abs_self _).trans (abs_min_sub_min_le_max _ _ _ _)

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