comp_eq_id

Mathlib.Logic.Function.Basic

URI: https://scilib.ai/kg/mathlib#Function.RightInverse.comp_eq_id

English

If f and g form a RightInverse pair, then g ∘ f = id.

Русский

Если f и g образуют правый обратныйм пары, то g ∘ f = id.

LaTeX

$$$\text{RightInverse}(f,g) \Rightarrow g \circ f = \mathrm{id}.$$$

Lean4

theorem comp_eq_id {f : α → β} {g : β → α} (h : RightInverse f g) : g ∘ f = id :=
  funext h

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

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

Разделы

Аффилиация

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