semiconj

Mathlib.Logic.Function.Conjugate

URI: https://scilib.ai/kg/mathlib#Function.Commute.semiconj

← MathLib Explorer

English

Reinterpret Commute f g as Semiconj f g g.

Русский

Переопределение Commute f g как Semiconj f g g.

LaTeX

$$$ \text{Semiconj}(f,g,g) $$$

Lean4

/-- Reinterpret `Function.Commute f g` as `Function.Semiconj f g g`. These two predicates are
definitionally equal but have different dot-notation lemmas. -/
theorem semiconj (h : Commute f g) : Semiconj f g g :=
  h

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

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

Разделы

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

Аффилиация

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