English
For any α and β, if β has SemilatticeInf, then OrderHom α β has SemilatticeInf structure with pointwise infimum.
Русский
Для любых α и β, если β имеет SemilatticeInf, то OrderHom α β обладает структурой SemilatticeInf, задаваемой точечным инфимумом.
LaTeX
$$$[SemilatticeInf\; β] ⇒ SemilatticeInf (OrderHom\; α\; β)$$$
Lean4
instance [SemilatticeInf β] : SemilatticeInf (α →o β) :=
{ (_ : PartialOrder (α →o β)), (dualIso α β).symm.toGaloisInsertion.liftSemilatticeInf with inf := (· ⊓ ·) }