rightInvOn — Mathlib

English

If f has a right inverse g, then on any set s, the right inverse relation holds, i.e., f is right-inverse of g on s.

Русский

Пусть у f есть правое обратное g; на любом множестве s f является правым обратным для g.

LaTeX

$$$\\text{RightInverse}\; f\; g \\Rightarrow \\text{RightInvOn}\; f\; g\\; s$$$

Lean4

theorem rightInvOn {g : β → α} (h : RightInverse f g) (s : Set α) : RightInvOn f g s := fun x _ => h x

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