symm_dual_comp — Mathlib

English

InfHom.symm_dual_comp (g : SupHom βᵒᵈ γᵒᵈ) (f : SupHom αᵒᵈ βᵒᵈ) : SupHom.dual.symm (g.comp f) = (SupHom.dual.symm g).comp (SupHom.dual.symm f).

Русский

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

LaTeX

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

Lean4

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

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