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 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).

Estimated changes

modified theorem set.diff_compl
modified theorem set.diff_self
modified theorem set.diff_subset
modified theorem set.inf_eq_inter
modified theorem set.le_eq_subset
modified theorem set.lt_eq_ssubset
modified theorem set.sup_eq_union
added theorem bot_sdiff
added theorem disjoint.sdiff_eq_left
added theorem disjoint_inf_sdiff
added theorem disjoint_sdiff
added theorem disjoint_sdiff_iff_le
added theorem disjoint_sdiff_sdiff
added theorem inf_inf_sdiff
added theorem inf_sdiff
added theorem inf_sdiff_assoc
added theorem inf_sdiff_eq_bot_iff
added theorem inf_sdiff_inf
added theorem inf_sdiff_left
added theorem inf_sdiff_right
added theorem inf_sdiff_self_left
added theorem inf_sdiff_self_right
added theorem inf_sdiff_sup_left
added theorem inf_sdiff_sup_right
added theorem le_iff_disjoint_sdiff
added theorem le_iff_eq_sup_sdiff
added theorem le_sdiff_sup
added theorem le_sup_sdiff
added theorem sdiff_bot
added theorem sdiff_compl
modified theorem sdiff_eq
added theorem sdiff_eq_bot_iff
deleted theorem sdiff_eq_left
added theorem sdiff_idem
deleted theorem sdiff_idem_right
added theorem sdiff_inf
added theorem sdiff_inf_sdiff
added theorem sdiff_inf_self_left
added theorem sdiff_inf_self_right
added theorem sdiff_le
added theorem sdiff_le_comm
added theorem sdiff_le_iff
added theorem sdiff_le_sdiff_self
added theorem sdiff_le_self_sdiff
added theorem sdiff_sdiff_comm
added theorem sdiff_sdiff_eq_self
added theorem sdiff_sdiff_left'
added theorem sdiff_sdiff_left
added theorem sdiff_sdiff_right'
added theorem sdiff_sdiff_right
added theorem sdiff_sdiff_right_self
added theorem sdiff_sdiff_sup_sdiff'
added theorem sdiff_sdiff_sup_sdiff
added theorem sdiff_self
added theorem sdiff_sup
added theorem sdiff_symm
added theorem sdiff_top
added theorem sdiff_unique
added theorem sup_inf_inf_sdiff
added theorem sup_inf_sdiff
added theorem sup_sdiff
added theorem sup_sdiff_cancel'
added theorem sup_sdiff_inf
added theorem sup_sdiff_left
added theorem sup_sdiff_left_self
added theorem sup_sdiff_of_le
added theorem sup_sdiff_right
added theorem sup_sdiff_right_self
deleted theorem sup_sdiff_same
added theorem sup_sdiff_self_left
added theorem sup_sdiff_self_right
added theorem sup_sdiff_symm
added theorem top_sdiff