instAssociativeCoeForallForallArrowCongr

English

Let e be a bijection between α₁ and β₁ and let f be an associative binary operation on α₁. Then the transported operation on β₁, defined by a ⋆ b := e( f( e^{-1}(a), e^{-1}(b) ) ), is associative.

Русский

Пусть e : α₁ ≃ β₁ — биекция, и f : α₁ × α₁ → α₁ — ассоциативная бинарная операция. Тогда перенесённая на β₁ операция, заданная a ⋆ b := e( f( e^{-1}(a), e^{-1}(b) ) ), ассоциативна.

LaTeX

$$$\\forall a,b,c \\in \\beta_1:\\; e\\big( f\\big( f( e^{-1}(a), e^{-1}(b) ), e^{-1}(c) \\big) \\big) = e\\big( f\\big( e^{-1}(a), f( e^{-1}(b), e^{-1}(c) ) \\big) \\big).$$$

Lean4

instance [Std.Associative f] : Std.Associative (e.arrowCongr (e.arrowCongr e) f) :=
  (e.semiconj₂_conj f).isAssociative_right e.surjective

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