injective_iff_hasLeftInverse

Mathlib.Logic.Function.Basic

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

English

Injective f is equivalent to HasLeftInverse f.

Русский

Инъективность f эквивалентна существованию левого обратного для f.

LaTeX

$$$ \text{Injective}(f) \leftrightarrow \text{HasLeftInverse}(f) $$$

Lean4

theorem injective_iff_hasLeftInverse : Injective f ↔ HasLeftInverse f :=
  ⟨Injective.hasLeftInverse, HasLeftInverse.injective⟩

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

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

Разделы

Аффилиация

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