rightInverse

Mathlib.Logic.Function.Basic

URI: https://scilib.ai/kg/mathlib#Function.LeftInverse.rightInverse

English

If g is a left inverse of f, then f has a right inverse g.

Русский

Если g является левым обратным к f, то f имеет правый обратный g.

LaTeX

$$$\forall f,g:\alpha \to \beta,\ \operatorname{LeftInverse}(g,f) \Rightarrow \operatorname{RightInverse}(f,g).$$$

Lean4

theorem rightInverse {f : α → β} {g : β → α} (h : LeftInverse g f) : RightInverse f g :=
  h

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

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

Разделы

Аффилиация

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