rightInverse_surjInv

Mathlib.Logic.Function.Basic

URI: https://scilib.ai/kg/mathlib#Function.rightInverse_surjInv

English

If f is surjective, then surjInv hf is a right inverse of f.

Русский

Если f сюръективна, то surjInv hf является правой обратной к f.

LaTeX

$$$ \text{Surjective}(f) \rightarrow \text{RightInverse}(\mathrm{surjInv}(hf), f) $$$

Lean4

theorem rightInverse_surjInv (hf : Surjective f) : RightInverse (surjInv hf) f :=
  surjInv_eq hf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru