dual_comp — Mathlib

English

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

Русский

Дуальная композиция g и f равна композиции дуалов двух отображений.

LaTeX

$$$\\text{dual} (g \\circ f) = \\text{dual}(g) \\circ \\text{dual}(f)$$$

Lean4

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

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