completeBooleanAlgebra — Mathlib

English

A simple bounded order yields a complemented lattice with Boolean operations.

Русский

Простой ограниченный порядок порождает дополненную решётку с булевыми операциями.

LaTeX

$$$\text{IsSimpleOrder.completeBooleanAlgebra}(\alpha)$$$

Lean4

/-- A simple `BoundedOrder` is also a `CompleteBooleanAlgebra`. -/
protected noncomputable def completeBooleanAlgebra : CompleteBooleanAlgebra α :=
  { __ := IsSimpleOrder.completeLattice
    __ := IsSimpleOrder.booleanAlgebra }

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