instBoundedOrder — Mathlib

English

If β is a bounded ordered set (i.e., has both bottom and top elements), then Germ l β is also a bounded ordered set. The bottom and top elements of Germ l β are obtained by taking germs of the bottom and top of β, respectively.

Русский

Если β обладает нижней и верхней границей, то Germ l β также является ограниченным упорядоченным множеством; нижний (resp. верхний) элемент Germ l β задаётся как germ нижнего (resp. верхнего) β.

LaTeX

$$$\\operatorname{BoundedOrder}(\\mathrm{Germ}_l \\beta)$$$

Lean4

instance instBoundedOrder [LE β] [BoundedOrder β] : BoundedOrder (Germ l β)
    where
  __ := instOrderBot
  __ := instOrderTop

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