dual_comp — Mathlib

English

Dualization converts composition of bounded lattice homomorphisms into the composition of duals: dual(g ∘ f) = (dual g) ∘ (dual f).

Русский

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

LaTeX

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

Lean4

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

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