commute — Mathlib

English

Reinterpret Semiconj f g g as Commute f g. They are definitionally equal in this context.

Русский

Переопределение Semiconj f g g как Commute f g. В этом контексте они по существу равны.

LaTeX

$$$ f \circ g = g \circ f $$$

Lean4

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

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