min_const — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem min_const (hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun x => min (f x) a :=
  hf.min (LocallyLipschitz.const a)

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