RightInvOn — Mathlib

English

`g` is a right inverse to `f` on `t` if `f(g(x)) = x` for all `x ∈ t`.

Русский

«g» является правым обратным к «f» на множестве t, если для каждого x ∈ t выполняется f(g(x)) = x.

LaTeX

$$$$ \\operatorname{RightInvOn}(g,f,t) \\iff \\forall x \\in t,\\ f(g(x)) = x $$$$

Lean4

/-- `g` is a right inverse to `f` on `t` if `f (g x) = x` for all `x ∈ t`. -/
abbrev RightInvOn (g : β → α) (f : α → β) (t : Set β) : Prop :=
  LeftInvOn f g t

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