symm_dual_comp — Mathlib

English

The inverse of dual of a composition equals the composition of inverses: dual.symm(g ∘ f) = dual.symm(g) ∘ dual.symm(f).

Русский

Обратная дуальности сохраняет композицию: дуал.symm(g ∘ f) = дуал.symm(g) ∘ дуал.symm(f).

LaTeX

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

Lean4

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

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