booleanAlgebra_of_sSup_eq_top — Mathlib

English

A compactly generated lattice with BooleanGenerators and top as sSup yields a Boolean algebra.

Русский

Компактно сгенерированная решётка с булевыми генераторами и топом как sSup порождает булеву алгебру.

LaTeX

$$$ \text{booleanAlgebraOfComplemented } α $$$

Lean4

/-- A compactly generated complete lattice generated by Boolean generators is a Boolean algebra. -/
noncomputable def booleanAlgebra_of_sSup_eq_top (hS : BooleanGenerators S) (h : sSup S = ⊤) : BooleanAlgebra α :=
  let _i := hS.distribLattice_of_sSup_eq_top h
  have := hS.complementedLattice_of_sSup_eq_top h
  DistribLattice.booleanAlgebraOfComplemented α

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