dual_comp — Mathlib

English

The dual of the composition of InfHom g and f equals the composition of the duals: sInfHom.dual (g.comp f) = (sInfHom.dual g).comp (sInfHom.dual f).

Русский

Дуальная композиция InfHom сохраняется: дуальная композиция g и f равна композиции их дуалов.

LaTeX

$$$sInfHom.dual (g.comp f) = (sInfHom.dual g).comp (sInfHom.dual f)$$$

Lean4

@[simp]
theorem dual_comp (g : sInfHom β γ) (f : sInfHom α β) :
    sInfHom.dual (g.comp f) = (sInfHom.dual g).comp (sInfHom.dual f) :=
  rfl

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