instBoundedOrder — Mathlib

English

If X is a semilattice with inf and has a top element, then the set of nuclei of X forms a bounded ordered set; equivalently, there are bottom and top nuclei providing a bounded order structure.

Русский

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

LaTeX

$$$([\\text{SemilatticeInf } X]) \\wedge ([\\text{OrderTop } X]) \\Rightarrow \\text{BoundedOrder}(\\mathrm{Nucleus}(X))$$$

Lean4

instance : BoundedOrder (Nucleus X) where
  bot_le _ _ := le_apply
  le_top _ _ := by simp

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