eqOn

Mathlib.Data.Set.Function

URI: https://scilib.ai/kg/mathlib#Set.RightInvOn.eqOn

English

If h is a RightInvOn f' f t, then EqOn (f ∘ f') id t.

Русский

Если h — правый обратный, то композиция f ∘ f' равна тождеству на t.

LaTeX

$$$$ \\text{EqOn } (f \\circ f') \\; \\mathrm{id} \\; t. $$$$

Lean4

theorem eqOn (h : RightInvOn f' f t) : EqOn (f ∘ f') id t :=
  h

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

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

Разделы

Аффилиация

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