min_const — Mathlib

English

If hf : LipschitzWith Kf f and a ∈ ℝ, then x ↦ min(a, f(x)) is Lipschitz with Kf.

Русский

Если hf — липшицев с константой Kf, и a ∈ ℝ, то min(a, f(x)) липшицево с Kf.

LaTeX

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

Lean4

theorem min_const (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun x => min (f x) a := by
  simpa only [max_eq_left (zero_le Kf)] using hf.min (LipschitzWith.const a)

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