Commit 2021-04-06 01:49 8e2db7fe
View on Github →refactor(order/boolean_algebra): generalized Boolean algebras (#6775)
We add "generalized Boolean algebras", following a suggestion of @jsm28. Now boolean_algebra
extends generalized_boolean_algebra
and boolean_algebra.core
:
class generalized_boolean_algebra (α : Type u) extends semilattice_sup_bot α, semilattice_inf_bot α,
distrib_lattice α, has_sdiff α :=
(sup_inf_sdiff : ∀a b:α, (a ⊓ b) ⊔ (a \ b) = a)
(inf_inf_sdiff : ∀a b:α, (a ⊓ b) ⊓ (a \ b) = ⊥)
class boolean_algebra.core (α : Type u) extends bounded_distrib_lattice α, has_compl α :=
(inf_compl_le_bot : ∀x:α, x ⊓ xᶜ ≤ ⊥)
(top_le_sup_compl : ∀x:α, ⊤ ≤ x ⊔ xᶜ)
class boolean_algebra (α : Type u) extends generalized_boolean_algebra α, boolean_algebra.core α :=
(sdiff_eq : ∀x y:α, x \ y = x ⊓ yᶜ)
I also added a module doc for order/boolean_algebra
.
Many lemmas about set difference both for finset
s and set
s now follow from their generalized_boolean_algebra
counterparts and I've removed the (fin)set-specific proofs.
finset.sdiff_subset_self
was removed in favor of the near-duplicate finset.sdiff_subset
(the latter has more explicit arguments).