lattice — Mathlib

English

If β is a lattice, then the space of order-preserving maps α →o β forms a lattice with pointwise supremum and infimum.

Русский

Если β — решетка, то множество отображений сохраняющих порядок образует решетку с точечно заданными операциями сверху и снизу.

LaTeX

$$$[Lattice\; β] ⇒ Lattice (OrderHom\; α\; β)$ with $(f ⊔ g)(a)=f(a) ⊔ g(a)$ and $(f ⊓ g)(a)=f(a) ⊓ g(a)$.$$

Lean4

instance lattice [Lattice β] : Lattice (α →o β) :=
  { (_ : SemilatticeSup (α →o β)), (_ : SemilatticeInf (α →o β)) with }

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