to_rightInvOn — Mathlib

English

If hf is AntilipschitzWith on f, and g is a right-inverse on t, then Lip_K g on t.restrict g.

Русский

Если антилипшицево на f и g является правой обратной на t, то Lip_K g на t.restrict g.

LaTeX

$$$AntilipschitzWith(K, f) \\Rightarrow ∀ g,t, RightInvOn g f t \\Rightarrow LipschitzWith(K, t.restrict g)$$$

Lean4

theorem to_rightInvOn (hf : AntilipschitzWith K f) {g : β → α} {t : Set β} (h : RightInvOn g f t) :
    LipschitzWith K (t.restrict g) :=
  (hf.restrict univ).to_rightInvOn' (mapsTo_univ g t) h

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