semiconj₂_conj — Mathlib

English

For an equivalence e, and a binary operation f, the semiconjugacy with respect to arrowCongr f is satisfied.

Русский

Для эквивалентности e и бинарной операции f выполняется semiconjugacy относительно arrowCongr e.conj f.

LaTeX

$$$\\text{Semiconj}_2\\ e\\ f\\ (e.\\text{arrowCongr}\\ e.\\text{conj}\\ f)$$$

Lean4

theorem semiconj₂_conj : Semiconj₂ e f (e.arrowCongr e.conj f) := fun x y => by simp [arrowCongr]

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