mono — Mathlib

English

If a function f is Lipschitz with constant K on a set t and s is contained in t, then f is Lipschitz with the same constant on s.

Русский

Если функция f Lipschitz с константой K на множестве t, и подмножество s ⊆ t, тогда f Lipschitz с той же константой на s.

LaTeX

$$$LipschitzOnWith(K,f,t)\ \land\ s\subseteq t\ \Rightarrow\ LipschitzOnWith(K,f,s)$$$

Lean4

/-- Being Lipschitz on a set is monotone w.r.t. that set. -/
theorem mono (hf : LipschitzOnWith K f t) (h : s ⊆ t) : LipschitzOnWith K f s := fun _x x_in _y y_in =>
  hf (h x_in) (h y_in)

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