comp_eq

Mathlib.Logic.Function.Conjugate

URI: https://scilib.ai/kg/mathlib#Function.Semiconj₂.comp_eq

English

Same as above: bicompr f ga equals bicompl gb f f under a Semiconj₂.

Русский

То же самое: bicompr f ga равно bicompl gb f f при Semiconj₂.

LaTeX

$$$ \text{bicompr } f ga = \text{bicompl } gb f f $$$

Lean4

protected theorem comp_eq (h : Semiconj₂ f ga gb) : bicompr f ga = bicompl gb f f :=
  funext fun x ↦ funext <| h x

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

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

Разделы

Аффилиация

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