leftInverse_of_rightInverse — Mathlib

English

If f is left inverse of g, then g is right inverse of f, providing a symmetry in inverse relations.

Русский

Если f — левый обратный к g, то g — правый обратный к f, демонстрируя симметрию отношений обратности.

LaTeX

$$$\text{LeftInverse}(f,g) \Rightarrow \text{RightInverse}(f,g)$$$

Lean4

theorem leftInverse_of_rightInverse (hfg : Function.RightInverse f g) : Function.LeftInverse f g :=
  rightInverse_of_leftInverse hfg

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