symm_dual_comp — Mathlib

English

The dual of the composition on dual orders satisfies the same rule as in item 161850, but in the dual setting.

Русский

Дуальная композиция над двойственными порядками удовлетворяет такое же правило, как и в пункте 161850, но в двойственном контексте.

LaTeX

$$$\\text{(g : sSupHom βᵒᵈ γᵒᵈ) (f : sSupHom αᵒᵈ βᵒᵈ)}\\;:\\; sSupHom.dual.symm (g.comp f) = (sSupHom.dual.symm g).comp (sSupHom.dual.symm f)$$$

Lean4

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

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