dual_comp — Mathlib

English

The dual of the composition of two sup-homomorphisms equals the composition of their duals: sSupHom.dual (g.comp f) = (sSupHom.dual g).comp (sSupHom.dual f).

Русский

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

LaTeX

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

Lean4

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

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