locallyLipschitzOn — Mathlib

English

If a function f is locally Lipschitz, then it is locally Lipschitz on any subset s of its domain when viewed as a restricted function.

Русский

Если функция локально липшицева, то она локально липшицева на любом подмножестве области, при рассмотрении ограниченной функции.

LaTeX

$$$LocallyLipschitz f\Rightarrow LocallyLipschitzOn s f$$$

Lean4

protected theorem locallyLipschitzOn (h : LocallyLipschitz f) : LocallyLipschitzOn s f :=
  (locallyLipschitzOn_univ.2 h).mono s.subset_univ

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