surjective_iff_hasRightInverse

Mathlib.Logic.Function.Basic

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

English

Surjectivity is equivalent to having a right inverse.

Русский

Сюръективность эквивалентна существованию правой обратной функции.

LaTeX

$$$ \text{Surjective}(f) \leftrightarrow \text{HasRightInverse}(f) $$$

Lean4

theorem surjective_iff_hasRightInverse : Surjective f ↔ HasRightInverse f :=
  ⟨Surjective.hasRightInverse, HasRightInverse.surjective⟩

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

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

Разделы

Аффилиация

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