symm_dual_comp — Mathlib

English

Symmetric dual composition identity for g and f with duals gives a commensurate equality as in item 161850.

Русский

Симметричная дуальная композиция даёт аналогичное равенство применительно к двойственным гомоморфизмам.

LaTeX

$$$sSupHom.dual.symm (g.comp f) = (sSupHom.dual.symm g).comp (sSupHom.dual.symm f)$$$

Lean4

@[simp]
theorem symm_dual_comp (g : CompleteLatticeHom βᵒᵈ γᵒᵈ) (f : CompleteLatticeHom αᵒᵈ βᵒᵈ) :
    CompleteLatticeHom.dual.symm (g.comp f) = (CompleteLatticeHom.dual.symm g).comp (CompleteLatticeHom.dual.symm f) :=
  rfl

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