instSupSet — Mathlib

English

If β is a complete lattice, then the supremum-collection of order-preserving maps forms a SupSet, with the supremum taken pointwise.

Русский

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

LaTeX

$$$[CompleteLattice\; β] : SupSet( OrderHom\; α\; β )$ with $\mathrm{sSup}(s)(x) = \sup_{f \in s} f(x).$$$

Lean4

instance [CompleteLattice β] : SupSet (α →o β) where
  sSup s := ⟨fun x => ⨆ f ∈ s, (f :) x, fun _ _ h => iSup₂_mono fun f _ => f.mono h⟩

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