English
Let α be a preorder and β a complete lattice. Then the collection of order-preserving maps from α to β, i.e. α →o β, forms a complete lattice under the pointwise order (top and bottom given by constant maps; suprema and infima are computed pointwise).
Русский
Пусть α — частично упорядоченное множество, а β — полная решетка. Тогда множество отображений, сохраняющих порядок, из α в β, образует полную решетку под точечным порядком; верхняя и нижняя границы задаются константными отображениями, а супремумы и инфимумы вычисляются покомпонентно.
LaTeX
$$$\\operatorname{CompleteLattice}(\\alpha \\to_o \\beta)$$$
Lean4
instance [CompleteLattice β] : CompleteLattice (α →o β) :=
{ (_ : Lattice (α →o β)), OrderHom.orderTop, OrderHom.orderBot with
-- Porting note: Added `by apply`, was `fun s f hf x => le_iSup_of_le f (le_iSup _ hf)`
le_sSup := fun s f hf x => le_iSup_of_le f (by apply le_iSup _ hf)
sSup_le := fun _ _ hf x => iSup₂_le fun g hg => hf g hg x
le_sInf := fun _ _ hf x => le_iInf₂ fun g hg => hf g hg x
sInf_le := fun _ f hf _ => iInf_le_of_le f (iInf_le _ hf) }
