lipschitzOnWith_iff_restrict — Mathlib

English

If h maps s into t, then LipschitzOnWith K f s is equivalent to LipschitzWith K (Set.MapsTo.restrict f s t).

Русский

Если h отображает s в t, то LipschitzOnWith K f s эквивалентно LipschitzWith K (Set.MapsTo.restrict f s t).

LaTeX

$$$MapsTo\ f\ s\ t\Rightarrow (LipschitzOnWith(K,f,s)\iff LipschitzWith(K,Set.MapsTo.restrict f s t))$$$

Lean4

theorem lipschitzOnWith_iff_restrict {t : Set β} (h : MapsTo f s t) :
    LipschitzOnWith K f s ↔ LipschitzWith K (h.restrict f s t) :=
  _root_.lipschitzOnWith_iff_restrict

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