English
For complete lattices α and β, the class of complete lattice homomorphisms from α to β is equipped with structure such that, for any homomorphism f, its action on suprema and infima is given by map_sSup' and map_sInf'. In other words, the class is closed under the standard preservation properties of suprema and infima.
Русский
Для полных решёток α и β множество всех гомоморфизмов по полной решетке α→β образует класс гомоморфизмов, сохраняющих пределы (супремумы и инфимумы); отображение в этом классе удовлетворяет свойствам сохранения верхних и нижних пределов.
LaTeX
$$$\\operatorname{map\\_sSup} f = f.map\\_sSup'\\quad\\text{и}\\quad \\operatorname{map\\_sInf} f = f.map\\_sInf'$, для каждого\, f \\,\\in\\, \\text{CompleteLatticeHom}(\\alpha,\\beta).$$$
Lean4
instance : CompleteLatticeHomClass (CompleteLatticeHom α β) α β
where
map_sSup f := f.map_sSup'
map_sInf f := f.map_sInf'
