dual_comp — Mathlib

English

The dual of the composition of two bounded-order homomorphisms is the composition of their duals.

Русский

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

LaTeX

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

Lean4

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

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