symm_dual_comp — Mathlib

English

Symmetric dual composition: (g ∘ f) under the dual-symmetry equals the composition of the duals with symm.

Русский

Композиция в дуальном виде сохраняется при симметричной дуальной операции над обоими аргументами.

LaTeX

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

Lean4

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

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