English
A map g is an inverse to f viewed as a map from s to t if it is a left inverse on s and a right inverse on t.
Русский
Глобальная inv: g является обратной к f как отображению из s в t, если g является левым обратным на s и правым обратным на t.
LaTeX
$$$$ \\operatorname{InvOn}(g,f,s,t) \\iff \\operatorname{LeftInvOn}(g,f,s) \\wedge \\operatorname{RightInvOn}(g,f,t) $$$$
Lean4
/-- `g` is an inverse to `f` viewed as a map from `s` to `t` -/
def InvOn (g : β → α) (f : α → β) (s : Set α) (t : Set β) : Prop :=
LeftInvOn g f s ∧ RightInvOn g f t