English
If hf : LipschitzWith Kf f and hg : LipschitzWith Kg g, then x ↦ max(f(x), g(x)) is Lipschitz with constant max(Kf, Kg).
Русский
Если hf и hg липшицевы с константами Kf и Kg, то max(f,g) липшицево с константой max(Kf,Kg).
LaTeX
$$$\\text{LipschitzWith}(\\max(K_f,K_g),\\, \\lambda x. \\max(f(x),g(x)))$$$
Lean4
/-- For functions to `ℝ`, it suffices to prove `f x ≤ f y + K * dist x y`; this version
doesn't assume `0≤K`. -/
protected theorem of_le_add_mul' {f : α → ℝ} (K : ℝ) (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y) :
LipschitzOnWith (Real.toNNReal K) f s :=
have I : ∀ x ∈ s, ∀ y ∈ s, f x - f y ≤ K * dist x y := fun x hx y hy => sub_le_iff_le_add'.2 (h x hx y hy)
LipschitzOnWith.of_dist_le' fun x hx y hy => abs_sub_le_iff.2 ⟨I x hx y hy, dist_comm y x ▸ I y hy x hx⟩
