rightInverse_of_leftInverse — Mathlib

English

For linear maps f: M → N and g: N → M, f is a left inverse of g iff f is a right inverse of g.

Русский

Для линейных отображений f: M → N и g: N → M, f является левым обратным к g тогда и только тогда, когда f является правым обратным к g.

LaTeX

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

Lean4

theorem rightInverse_of_leftInverse (hfg : Function.LeftInverse f g) : Function.RightInverse f g :=
  Function.rightInverse_of_injective_of_leftInverse (bijective_of_surjective hfg.surjective).injective hfg

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