English
There is a canonical equivalence between bounded lattice homomorphisms and those between dual lattices.
Русский
Существует каноническое соответствие между гомоморфизмами ограниченной решетки и гомоморфизмами между дуальными решетками.
LaTeX
$$$ \\mathrm{BoundedLatticeHom} (α, β) \\simeq \\mathrm{BoundedLatticeHom}(α^{\\mathrm{op}}, β^{\\mathrm{op}}) $$$
Lean4
instance (priority := 100) toInfTopHomClass [CompleteLattice α] [CompleteLattice β] [sInfHomClass F α β] :
InfTopHomClass F α β :=
{
‹sInfHomClass F α
β› with
map_inf := fun f a b => by
rw [← sInf_pair, map_sInf, Set.image_pair]
simp only [sInf_insert, sInf_singleton]
map_top := fun f => by rw [← sInf_empty, map_sInf, Set.image_empty, sInf_empty] }
-- See note [lower instance priority]
