toBoundedOrder — Mathlib

English

Every Boolean algebra α carries a natural bounded order structure; it is a bounded lattice with bottom and top elements.

Русский

Каждая булева алгебра α естественным образом имеет ограниченный порядок; это ограниченная решётка с нулём и единицей.

LaTeX

$$$[\text{BooleanAlgebra}(\alpha)] \Rightarrow [\text{BoundedOrder}(\alpha)].$$$

Lean4

instance (priority := 100) toBoundedOrder [h : BooleanAlgebra α] : BoundedOrder α :=
  { h with }

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