InvOn — Mathlib

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

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