hasRightInverse

Mathlib.Logic.Function.Basic

URI: https://scilib.ai/kg/mathlib#Function.Surjective.hasRightInverse

English

If f is surjective, then f has a right inverse.

Русский

Если f сюръективна, то у f есть правое обратное.

LaTeX

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

Lean4

theorem hasRightInverse (hf : Surjective f) : HasRightInverse f :=
  ⟨_, rightInverse_surjInv hf⟩

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

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

Разделы

Аффилиация

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