to_rightInvOn' — Mathlib

English

If hf is AntilipschitzWith on s.restrict f, and g maps t into s with a right-inverse on t, then t.restrict g is Lipschitz with the same constant.

Русский

Если hf антилипшицево на s.restrict f и g переводит t в s и имеет обратную справа инверсию, то t.restrict g обратно Lipschitz.

LaTeX

$$$\\forall x,y,\\, LipschitzWith(K, t.restrict g)$$$

Lean4

theorem to_rightInvOn' {s : Set α} (hf : AntilipschitzWith K (s.restrict f)) {g : β → α} {t : Set β}
    (g_maps : MapsTo g t s) (g_inv : RightInvOn g f t) : LipschitzWith K (t.restrict g) := fun x y => by
  simpa only [restrict_apply, g_inv x.mem, g_inv y.mem, Subtype.edist_mk_mk] using
    hf ⟨g x, g_maps x.mem⟩ ⟨g y, g_maps y.mem⟩

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