Commit 2021-04-06 01:49 8e2db7fe

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 finsets and sets 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).