locallyLipschitz — Mathlib

English

If a function is Lipschitz with some constant K, then it is locally Lipschitz.

Русский

Если функция липшицева с константой K, то она локально липшицева.

LaTeX

$$$\\forall f, \\forall K \\,( LipschitzWith K f \\Rightarrow LocallyLipschitz f)$$$

Lean4

/-- A Lipschitz function is locally Lipschitz. -/
protected theorem _root_.LipschitzWith.locallyLipschitz {K : ℝ≥0} (hf : LipschitzWith K f) : LocallyLipschitz f :=
  fun _ ↦ ⟨K, univ, Filter.univ_mem, lipschitzOnWith_univ.mpr hf⟩

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