toBooleanAlgebra — Mathlib

English

A bounded generalized Boolean algebra is a Boolean algebra.

Русский

Если обобщённая булева алгебра ограничена сверху и снизу, она является булевой алгеброй.

LaTeX

$$$\\alpha \\text{ bounded generalized Boolean algebra } \\Rightarrow \\text{Boolean algebra }(\\alpha)$$$

Lean4

/-- A bounded generalized Boolean algebra is a Boolean algebra. -/
abbrev toBooleanAlgebra [GeneralizedBooleanAlgebra α] [OrderTop α] : BooleanAlgebra α
    where
  __ := ‹GeneralizedBooleanAlgebra α›
  __ := GeneralizedBooleanAlgebra.toOrderBot
  __ := ‹OrderTop α›
  compl a := ⊤ \ a
  inf_compl_le_bot _ := disjoint_sdiff_self_right.le_bot
  top_le_sup_compl _ := le_sup_sdiff
  sdiff_eq a
    b := by
    change _ = a ⊓ (⊤ \ b)
    rw [← inf_sdiff_assoc, inf_top_eq]

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