conjBy_trans — Mathlib

English

Conjugating by a composition of order isomorphisms equals successively conjugating by each isomorphism.

Русский

Конъюгация по композиции би-дополнения равна конъюгации по каждому из факторов по отдельности.

LaTeX

$$$c.conjBy( e_{1}.trans e_{2}) = (c.conjBy e_{1}).conjBy e_{2}$$$

Lean4

theorem conjBy_trans {α β γ} [Preorder α] [Preorder β] [Preorder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ)
    (c : ClosureOperator α) : c.conjBy (e₁.trans e₂) = (c.conjBy e₁).conjBy e₂ :=
  rfl

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