symm_dual_comp — Mathlib

English

The symm.dual respects composition: (g ≫ f)ᵈ = (gᵈ ≫ fᵈ).

Русский

Симметричная двойственность сохраняет композицию: (g ∘ f)ᵈ = gᵈ ∘ fᵈ.

LaTeX

$$$\mathrm{BoundedOrderHom.dual.symm}(g \circ f) = (\mathrm{BoundedOrderHom.dual.symm}\, g) \circ (\mathrm{BoundedOrderHom.dual.symm}\, f)$$$

Lean4

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

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