eq

Mathlib.Logic.Function.Conjugate

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

← MathLib Explorer

English

If h is a semiconjugacy, then h(x) satisfies f(ga x) = gb(f x).

Русский

Если h — полусопряжение, то выполняется f(ga x) = gb(f x).

LaTeX

$$$ \forall {\alpha} {\beta} {\gamma} {f : \alpha \to \beta} {ga : \alpha \to \alpha} {gb : \beta \to \beta} (h : \operatorname{Semiconj} f ga gb) (x : \alpha),\; f (ga x) = gb (f x)$$$

Lean4

protected theorem eq (h : Semiconj f ga gb) (x : α) : f (ga x) = gb (f x) :=
  h x

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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