instIdempotentOpCoeForallForallArrowCongr

English

Let f be an idempotent binary operation on α and e: α ≃ β. Then the transported operation on β, defined by a ⋆ b := e( f( e^{-1}(a), e^{-1}(b) ) ), is idempotent; i.e., a ⋆ a = a for all a ∈ β.

Русский

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

LaTeX

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

Lean4

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

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