of_le_add_mul — Mathlib

English

If hf : LipschitzWith Kf f and hg : LipschitzWith Kg g, then x ↦ min(f(x), g(x)) is Lipschitz with constant max(Kf, Kg).

Русский

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

LaTeX

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

Lean4

/-- For functions to `ℝ`, it suffices to prove `f x ≤ f y + K * dist x y`; this version
assumes `0≤K`. -/
protected theorem of_le_add_mul {f : α → ℝ} (K : ℝ≥0) (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y) :
    LipschitzOnWith K f s := by simpa only [Real.toNNReal_coe] using LipschitzOnWith.of_le_add_mul' K h

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