mono — Mathlib

English

If a function is locally Lipschitz on a set t and s ⊆ t, then it is locally Lipschitz on s.

Русский

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

LaTeX

$$$LocallyLipschitzOn(t,f)\ \land\ s\subseteq t\ \Rightarrow\ LocallyLipschitzOn(s,f)$$$

Lean4

theorem mono (hf : LocallyLipschitzOn t f) (h : s ⊆ t) : LocallyLipschitzOn s f := fun x hx ↦ by
  obtain ⟨K, u, hu, hfu⟩ := hf (h hx); exact ⟨K, u, nhdsWithin_mono _ h hu, hfu⟩

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