const_min — Mathlib

English

If f is locally Lipschitz, then x ↦ min(a, f(x)) is locally Lipschitz for any a ∈ ℝ.

Русский

Если f локально липшицево, то x ↦ min(a, f(x)) локально липшицево для любого a ∈ ℝ.

LaTeX

$$$(\\text{LocallyLipschitz} f) \\Rightarrow \\forall a \\in \\mathbb{R}, \\text{LocallyLipschitz}\\big( x \\mapsto \\min(a, f(x))\\big).$$$

Lean4

theorem const_min (hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun x => min a (f x) := by
  simpa [min_comm] using (hf.min_const a)

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