Documentation

Mathlib.Order.BooleanAlgebra

(Generalized) Boolean algebras #

A Boolean algebra is a bounded distributive lattice with a complement operator. Boolean algebras generalize the (classical) logic of propositions and the lattice of subsets of a set.

Generalized Boolean algebras may be less familiar, but they are essentially Boolean algebras which do not necessarily have a top element () (and hence not all elements may have complements). One example in mathlib is Finset α, the type of all finite subsets of an arbitrary (not-necessarily-finite) type α.

GeneralizedBooleanAlgebra α is defined to be a distributive lattice with bottom () admitting a relative complement operator, written using "set difference" notation as x \ y (sdiff x y). For convenience, the BooleanAlgebra type class is defined to extend GeneralizedBooleanAlgebra so that it is also bundled with a \ operator.

(A terminological point: x \ y is the complement of y relative to the interval [⊥, x]. We do not yet have relative complements for arbitrary intervals, as we do not even have lattice intervals.)

Main declarations #

Implementation notes #

The sup_inf_sdiff and inf_inf_sdiff axioms for the relative complement operator in GeneralizedBooleanAlgebra are taken from Wikipedia.

[Stone's paper introducing generalized Boolean algebras][Stone1935] does not define a relative complement operator a \ b for all a, b. Instead, the postulates there amount to an assumption that for all a, b : α where a ≤ b, the equations x ⊔ a = b and x ⊓ a = ⊥ have a solution x. Disjoint.sdiff_unique proves that this x is in fact b \ a.

References #

Tags #

generalized Boolean algebras, Boolean algebras, lattices, sdiff, compl

Generalized Boolean algebras #

Some of the lemmas in this section are from:

class GeneralizedBooleanAlgebra (α : Type u) extends DistribLattice α, SDiff α, Bot α :

A generalized Boolean algebra is a distributive lattice with and a relative complement operation \ (called sdiff, after "set difference") satisfying (a ⊓ b) ⊔ (a \ b) = a and (a ⊓ b) ⊓ (a \ b) = ⊥, i.e. a \ b is the complement of b in a.

This is a generalization of Boolean algebras which applies to Finset α for arbitrary (not-necessarily-Fintype) α.

Instances
    @[simp]
    theorem sup_inf_sdiff {α : Type u} [GeneralizedBooleanAlgebra α] (x y : α) :
    xyx \ y = x
    @[simp]
    theorem inf_inf_sdiff {α : Type u} [GeneralizedBooleanAlgebra α] (x y : α) :
    xyx \ y =
    @[simp]
    theorem sup_sdiff_inf {α : Type u} [GeneralizedBooleanAlgebra α] (x y : α) :
    x \ yxy = x
    @[simp]
    theorem inf_sdiff_inf {α : Type u} [GeneralizedBooleanAlgebra α] (x y : α) :
    x \ y(xy) =
    @[instance 100]
    Equations
      theorem disjoint_inf_sdiff {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] :
      Disjoint (xy) (x \ y)
      theorem sdiff_unique {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (s : xyz = x) (i : xyz = ) :
      x \ y = z
      @[simp]
      theorem sdiff_inf_sdiff {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] :
      x \ yy \ x =
      theorem disjoint_sdiff_sdiff {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] :
      Disjoint (x \ y) (y \ x)
      @[simp]
      theorem inf_sdiff_self_right {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] :
      xy \ x =
      @[simp]
      theorem inf_sdiff_self_left {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] :
      y \ xx =
      theorem disjoint_sdiff_self_left {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] :
      Disjoint (y \ x) x
      theorem disjoint_sdiff_self_right {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] :
      Disjoint x (y \ x)
      theorem le_sdiff {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] :
      x y \ z x y Disjoint x z
      @[simp]
      theorem sdiff_eq_left {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] :
      x \ y = x Disjoint x y
      theorem Disjoint.sdiff_eq_of_sup_eq {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hi : Disjoint x z) (hs : xz = y) :
      y \ x = z
      theorem Disjoint.sdiff_unique {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hd : Disjoint x z) (hz : z y) (hs : y xz) :
      y \ x = z
      theorem disjoint_sdiff_iff_le {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hz : z y) (hx : x y) :
      Disjoint z (y \ x) z x
      theorem le_iff_disjoint_sdiff {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hz : z y) (hx : x y) :
      z x Disjoint z (y \ x)
      theorem inf_sdiff_eq_bot_iff {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hz : z y) (hx : x y) :
      zy \ x = z x
      theorem le_iff_eq_sup_sdiff {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hz : z y) (hx : x y) :
      x z y = zy \ x
      theorem sdiff_sup {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] :
      y \ (xz) = y \ xy \ z
      theorem sdiff_eq_sdiff_iff_inf_eq_inf {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] :
      y \ x = y \ z yx = yz
      theorem sdiff_eq_self_iff_disjoint {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] :
      x \ y = x Disjoint y x
      theorem sdiff_eq_self_iff_disjoint' {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] :
      x \ y = x Disjoint x y
      theorem sdiff_lt {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] (hx : y x) (hy : y ) :
      x \ y < x
      theorem sdiff_lt_left {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] :
      x \ y < x ¬Disjoint y x
      @[simp]
      theorem le_sdiff_right {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] :
      x y \ x x =
      @[simp]
      theorem sdiff_eq_right {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] :
      x \ y = y x = y =
      theorem sdiff_ne_right {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] :
      x \ y y x y
      theorem sdiff_lt_sdiff_right {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (h : x < y) (hz : z x) :
      x \ z < y \ z
      theorem sup_inf_inf_sdiff {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] :
      xyzy \ z = xyy \ z
      theorem sdiff_sdiff_right {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] :
      x \ (y \ z) = x \ yxyz
      theorem sdiff_sdiff_right' {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] :
      x \ (y \ z) = x \ yxz
      theorem sdiff_sdiff_eq_sdiff_sup {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (h : z x) :
      x \ (y \ z) = x \ yz
      @[simp]
      theorem sdiff_sdiff_right_self {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] :
      x \ (x \ y) = xy
      theorem sdiff_sdiff_eq_self {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] (h : y x) :
      x \ (x \ y) = y
      theorem sdiff_eq_symm {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hy : y x) (h : x \ y = z) :
      x \ z = y
      theorem sdiff_eq_comm {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hy : y x) (hz : z x) :
      x \ y = z x \ z = y
      theorem eq_of_sdiff_eq_sdiff {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hxz : x z) (hyz : y z) (h : z \ x = z \ y) :
      x = y
      theorem sdiff_le_sdiff_iff_le {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hx : x z) (hy : y z) :
      z \ x z \ y y x
      theorem sdiff_sdiff_left' {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] :
      (x \ y) \ z = x \ yx \ z
      theorem sdiff_sdiff_sup_sdiff {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] :
      z \ (x \ yy \ x) = z(z \ xy)(z \ yx)
      theorem sdiff_sdiff_sup_sdiff' {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] :
      z \ (x \ yy \ x) = zxyz \ xz \ y
      theorem sdiff_sdiff_sdiff_cancel_left {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hca : z x) :
      (x \ y) \ (x \ z) = z \ y
      theorem sdiff_sdiff_sdiff_cancel_right {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (hcb : z y) :
      (x \ z) \ (y \ z) = x \ y
      theorem inf_sdiff {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] :
      (xy) \ z = x \ zy \ z
      theorem inf_sdiff_assoc {α : Type u} [GeneralizedBooleanAlgebra α] (x y z : α) :
      (xy) \ z = xy \ z

      See also sdiff_inf_right_comm.

      theorem sdiff_inf_right_comm {α : Type u} [GeneralizedBooleanAlgebra α] (x y z : α) :
      x \ zy = (xy) \ z

      See also inf_sdiff_assoc.

      theorem inf_sdiff_left_comm {α : Type u} [GeneralizedBooleanAlgebra α] (a b c : α) :
      ab \ c = ba \ c
      @[deprecated sdiff_inf_right_comm (since := "2025-01-08")]
      theorem inf_sdiff_right_comm {α : Type u} [GeneralizedBooleanAlgebra α] (x y z : α) :
      x \ zy = (xy) \ z

      Alias of sdiff_inf_right_comm.


      See also inf_sdiff_assoc.

      theorem inf_sdiff_distrib_left {α : Type u} [GeneralizedBooleanAlgebra α] (a b c : α) :
      ab \ c = (ab) \ (ac)
      theorem inf_sdiff_distrib_right {α : Type u} [GeneralizedBooleanAlgebra α] (a b c : α) :
      a \ bc = (ac) \ (bc)
      theorem disjoint_sdiff_comm {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] :
      Disjoint (x \ z) y Disjoint x (y \ z)
      theorem sup_eq_sdiff_sup_sdiff_sup_inf {α : Type u} {x y : α} [GeneralizedBooleanAlgebra α] :
      xy = x \ yy \ xxy
      theorem sup_lt_of_lt_sdiff_left {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (h : y < z \ x) (hxz : x z) :
      xy < z
      theorem sup_lt_of_lt_sdiff_right {α : Type u} {x y z : α} [GeneralizedBooleanAlgebra α] (h : x < z \ y) (hyz : y z) :
      xy < z
      instance Pi.instGeneralizedBooleanAlgebra {ι : Type u_2} {α : ιType u_3} [(i : ι) → GeneralizedBooleanAlgebra (α i)] :
      GeneralizedBooleanAlgebra ((i : ι) → α i)
      Equations

        Boolean algebras #

        class BooleanAlgebra (α : Type u) extends DistribLattice α, HasCompl α, SDiff α, HImp α, Top α, Bot α :

        A Boolean algebra is a bounded distributive lattice with a complement operator such that x ⊓ xᶜ = ⊥ and x ⊔ xᶜ = ⊤. For convenience, it must also provide a set difference operation \ and a Heyting implication satisfying x \ y = x ⊓ yᶜ and x ⇨ y = y ⊔ xᶜ.

        This is a generalization of (classical) logic of propositions, or the powerset lattice.

        Since BoundedOrder, OrderBot, and OrderTop are mixins that require LE to be present at define-time, the extends mechanism does not work with them. Instead, we extend using the underlying Bot and Top data typeclasses, and replicate the order axioms of those classes here. A "forgetful" instance back to BoundedOrder is provided.

        Instances
          @[instance 100]
          Equations
            @[reducible, inline]

            A bounded generalized boolean algebra is a boolean algebra.

            Equations
              Instances For
                theorem inf_compl_eq_bot' {α : Type u} {x : α} [BooleanAlgebra α] :
                xx =
                @[simp]
                theorem sup_compl_eq_top {α : Type u} {x : α} [BooleanAlgebra α] :
                xx =
                @[simp]
                theorem compl_sup_eq_top {α : Type u} {x : α} [BooleanAlgebra α] :
                xx =
                theorem isCompl_compl {α : Type u} {x : α} [BooleanAlgebra α] :
                theorem sdiff_eq {α : Type u} {x y : α} [BooleanAlgebra α] :
                x \ y = xy
                theorem himp_eq {α : Type u} {x y : α} [BooleanAlgebra α] :
                x y = yx
                @[instance 100]
                Equations
                  @[simp]
                  theorem hnot_eq_compl {α : Type u} {x : α} [BooleanAlgebra α] :
                  theorem top_sdiff {α : Type u} {x : α} [BooleanAlgebra α] :
                  \ x = x
                  theorem eq_compl_iff_isCompl {α : Type u} {x y : α} [BooleanAlgebra α] :
                  x = y IsCompl x y
                  theorem compl_eq_iff_isCompl {α : Type u} {x y : α} [BooleanAlgebra α] :
                  x = y IsCompl x y
                  theorem compl_eq_comm {α : Type u} {x y : α} [BooleanAlgebra α] :
                  x = y y = x
                  theorem eq_compl_comm {α : Type u} {x y : α} [BooleanAlgebra α] :
                  x = y y = x
                  @[simp]
                  theorem compl_compl {α : Type u} [BooleanAlgebra α] (x : α) :
                  @[simp]
                  theorem compl_inj_iff {α : Type u} {x y : α} [BooleanAlgebra α] :
                  x = y x = y
                  theorem IsCompl.compl_eq_iff {α : Type u} {x y z : α} [BooleanAlgebra α] (h : IsCompl x y) :
                  z = y z = x
                  @[simp]
                  theorem compl_eq_top {α : Type u} {x : α} [BooleanAlgebra α] :
                  @[simp]
                  theorem compl_eq_bot {α : Type u} {x : α} [BooleanAlgebra α] :
                  @[simp]
                  theorem compl_inf {α : Type u} {x y : α} [BooleanAlgebra α] :
                  (xy) = xy
                  @[simp]
                  theorem compl_le_compl_iff_le {α : Type u} {x y : α} [BooleanAlgebra α] :
                  y x x y
                  @[simp]
                  theorem compl_lt_compl_iff_lt {α : Type u} {x y : α} [BooleanAlgebra α] :
                  y < x x < y
                  theorem compl_le_of_compl_le {α : Type u} {x y : α} [BooleanAlgebra α] (h : y x) :
                  x y
                  theorem compl_le_iff_compl_le {α : Type u} {x y : α} [BooleanAlgebra α] :
                  x y y x
                  @[simp]
                  theorem compl_le_self {α : Type u} {x : α} [BooleanAlgebra α] :
                  x x x =
                  @[simp]
                  theorem compl_lt_self {α : Type u} {x : α} [BooleanAlgebra α] [Nontrivial α] :
                  x < x x =
                  @[simp]
                  theorem sdiff_compl {α : Type u} {x y : α} [BooleanAlgebra α] :
                  x \ y = xy
                  @[simp]
                  theorem sup_inf_inf_compl {α : Type u} {x y : α} [BooleanAlgebra α] :
                  xyxy = x
                  theorem compl_sdiff {α : Type u} {x y : α} [BooleanAlgebra α] :
                  (x \ y) = x y
                  @[simp]
                  theorem compl_himp {α : Type u} {x y : α} [BooleanAlgebra α] :
                  (x y) = x \ y
                  theorem compl_sdiff_compl {α : Type u} {x y : α} [BooleanAlgebra α] :
                  x \ y = y \ x
                  @[simp]
                  theorem compl_himp_compl {α : Type u} {x y : α} [BooleanAlgebra α] :
                  x y = y x
                  theorem disjoint_compl_left_iff {α : Type u} {x y : α} [BooleanAlgebra α] :
                  theorem disjoint_compl_right_iff {α : Type u} {x y : α} [BooleanAlgebra α] :
                  theorem codisjoint_himp_self_left {α : Type u} {x y : α} [BooleanAlgebra α] :
                  Codisjoint (x y) x
                  theorem codisjoint_himp_self_right {α : Type u} {x y : α} [BooleanAlgebra α] :
                  Codisjoint x (x y)
                  theorem himp_le {α : Type u} {x y z : α} [BooleanAlgebra α] :
                  x y z y z Codisjoint x z
                  @[simp]
                  theorem himp_le_left {α : Type u} {x y : α} [BooleanAlgebra α] :
                  x y x x =
                  @[simp]
                  theorem himp_eq_left {α : Type u} {x y : α} [BooleanAlgebra α] :
                  x y = x x = y =
                  theorem himp_ne_right {α : Type u} {x y : α} [BooleanAlgebra α] :
                  x y x x y
                  instance Prod.instBooleanAlgebra {α : Type u} {β : Type u_1} [BooleanAlgebra α] [BooleanAlgebra β] :
                  Equations
                    instance Pi.instBooleanAlgebra {ι : Type u} {α : ιType v} [(i : ι) → BooleanAlgebra (α i)] :
                    BooleanAlgebra ((i : ι) → α i)
                    Equations
                      theorem Bool.sup_eq_bor :
                      (fun (x1 x2 : Bool) => max x1 x2) = or
                      theorem Bool.inf_eq_band :
                      (fun (x1 x2 : Bool) => min x1 x2) = and
                      @[reducible, inline]
                      abbrev Function.Injective.generalizedBooleanAlgebra {α : Type u} {β : Type u_1} [Max α] [Min α] [Bot α] [SDiff α] [GeneralizedBooleanAlgebra β] (f : αβ) (hf : Injective f) (map_sup : ∀ (a b : α), f (ab) = f af b) (map_inf : ∀ (a b : α), f (ab) = f af b) (map_bot : f = ) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) :

                      Pullback a GeneralizedBooleanAlgebra along an injection.

                      Equations
                        Instances For
                          @[reducible, inline]
                          abbrev Function.Injective.booleanAlgebra {α : Type u} {β : Type u_1} [Max α] [Min α] [Top α] [Bot α] [HasCompl α] [SDiff α] [HImp α] [BooleanAlgebra β] (f : αβ) (hf : Injective f) (map_sup : ∀ (a b : α), f (ab) = f af b) (map_inf : ∀ (a b : α), f (ab) = f af b) (map_top : f = ) (map_bot : f = ) (map_compl : ∀ (a : α), f a = (f a)) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) (map_himp : ∀ (a b : α), f (a b) = f a f b) :

                          Pullback a BooleanAlgebra along an injection.

                          Equations
                            Instances For

                              An alternative constructor for boolean algebras: a distributive lattice that is complemented is a boolean algebra.

                              This is not an instance, because it creates data using choice.

                              Equations
                                Instances For