English
Bounded lattice homomorphisms admit a dual correspondence with dual bounded lattices: a canonical equivalence BoundedLatticeHom α β ≃ BoundedLatticeHom αᵒᵈ βᵒᵈ.
Русский
Гомоморфизмы ограниченной решетки имеют каноническое соответствие с гомоморфизмами дуальных ограниченных решеток: эквивалентность BoundedLatticeHom α β ≃ BoundedLatticeHom αᵒᵈ βᵒᵈ.
LaTeX
$$$ \\mathrm{BoundedLatticeHom} (α, β) \\cong \\mathrm{BoundedLatticeHom}(α^{\\mathrm{op}}, β^{\\mathrm{op}}) $$$
Lean4
/-- Reinterpret a bounded lattice homomorphism as a bounded lattice homomorphism between the dual
bounded lattices. -/
@[simps]
protected def dual : BoundedLatticeHom α β ≃ BoundedLatticeHom αᵒᵈ βᵒᵈ
where
toFun f := ⟨LatticeHom.dual f.toLatticeHom, f.map_bot', f.map_top'⟩
invFun f := ⟨LatticeHom.dual.symm f.toLatticeHom, f.map_bot', f.map_top'⟩
