instSemilatticeInf — Mathlib

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 := (· ⊓ ·) }

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