comp_eq_id

Mathlib.Logic.Function.Basic

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

English

If g is a left inverse of f, then f ∘ g equals the identity on the domain.

Русский

Если g — левый обратный к f, то f ∘ g = id.

LaTeX

$$$\text{If } h: \text{LeftInverse}(f,g),\text{ then } f \circ g = \mathrm{id}.$$$

Lean4

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

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

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

Разделы

Аффилиация

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