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:

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

  • sup : ααα
  • le : ααProp
  • lt : ααProp
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • le_sup_left : ∀ (a b : α), a a b
  • le_sup_right : ∀ (a b : α), b a b
  • sup_le : ∀ (a b c : α), a cb ca b c
  • inf : ααα
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c : α), a ba ca b c
  • le_sup_inf : ∀ (x y z : α), (x y) (x z) x y z
  • sdiff : ααα
  • bot : α
  • sup_inf_sdiff : ∀ (a b : α), a b a \ b = a

    For any a, b, (a ⊓ b) ⊔ (a / b) = a

  • inf_inf_sdiff : ∀ (a b : α), a b a \ b =

    For any a, b, (a ⊓ b) ⊓ (a / b) = ⊥

Instances
    @[simp]
    theorem sup_inf_sdiff {α : Type u} [GeneralizedBooleanAlgebra α] (x : α) (y : α) :
    x y x \ y = x
    @[simp]
    theorem inf_inf_sdiff {α : Type u} [GeneralizedBooleanAlgebra α] (x : α) (y : α) :
    x y x \ y =
    @[simp]
    theorem sup_sdiff_inf {α : Type u} [GeneralizedBooleanAlgebra α] (x : α) (y : α) :
    x \ y x y = x
    @[simp]
    theorem inf_sdiff_inf {α : Type u} [GeneralizedBooleanAlgebra α] (x : α) (y : α) :
    x \ y (x y) =
    Equations
    • GeneralizedBooleanAlgebra.toOrderBot = let __spread.0 := GeneralizedBooleanAlgebra.toBot; OrderBot.mk
    theorem disjoint_inf_sdiff {α : Type u} {x : α} {y : α} [GeneralizedBooleanAlgebra α] :
    Disjoint (x y) (x \ y)
    theorem sdiff_unique {α : Type u} {x : α} {y : α} {z : α} [GeneralizedBooleanAlgebra α] (s : x y z = x) (i : x y z = ) :
    x \ y = z
    @[simp]
    theorem sdiff_inf_sdiff {α : Type u} {x : α} {y : α} [GeneralizedBooleanAlgebra α] :
    x \ y y \ 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 α] :
    x y \ x =
    @[simp]
    theorem inf_sdiff_self_left {α : Type u} {x : α} {y : α} [GeneralizedBooleanAlgebra α] :
    y \ x x =
    Equations
    • GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra = let __spread.0 := inst; let __spread.1 := GeneralizedBooleanAlgebra.toOrderBot; GeneralizedCoheytingAlgebra.mk
    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 : x z = y) :
    y \ x = z
    theorem Disjoint.sdiff_unique {α : Type u} {x : α} {y : α} {z : α} [GeneralizedBooleanAlgebra α] (hd : Disjoint x z) (hz : z y) (hs : y x z) :
    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) :
    z y \ x = z x
    theorem le_iff_eq_sup_sdiff {α : Type u} {x : α} {y : α} {z : α} [GeneralizedBooleanAlgebra α] (hz : z y) (hx : x y) :
    x z y = z y \ x
    theorem sdiff_sup {α : Type u} {x : α} {y : α} {z : α} [GeneralizedBooleanAlgebra α] :
    y \ (x z) = y \ x y \ z
    theorem sdiff_eq_sdiff_iff_inf_eq_inf {α : Type u} {x : α} {y : α} {z : α} [GeneralizedBooleanAlgebra α] :
    y \ x = y \ z y x = y z
    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
    @[simp]
    theorem le_sdiff_iff {α : 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 α] :
    x y z y \ z = x y y \ z
    theorem sdiff_sdiff_right {α : Type u} {x : α} {y : α} {z : α} [GeneralizedBooleanAlgebra α] :
    x \ (y \ z) = x \ y x y z
    theorem sdiff_sdiff_right' {α : Type u} {x : α} {y : α} {z : α} [GeneralizedBooleanAlgebra α] :
    x \ (y \ z) = x \ y x z
    theorem sdiff_sdiff_eq_sdiff_sup {α : Type u} {x : α} {y : α} {z : α} [GeneralizedBooleanAlgebra α] (h : z x) :
    x \ (y \ z) = x \ y z
    @[simp]
    theorem sdiff_sdiff_right_self {α : Type u} {x : α} {y : α} [GeneralizedBooleanAlgebra α] :
    x \ (x \ y) = x y
    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_sdiff_left' {α : Type u} {x : α} {y : α} {z : α} [GeneralizedBooleanAlgebra α] :
    (x \ y) \ z = x \ y x \ z
    theorem sdiff_sdiff_sup_sdiff {α : Type u} {x : α} {y : α} {z : α} [GeneralizedBooleanAlgebra α] :
    z \ (x \ y y \ x) = z (z \ x y) (z \ y x)
    theorem sdiff_sdiff_sup_sdiff' {α : Type u} {x : α} {y : α} {z : α} [GeneralizedBooleanAlgebra α] :
    z \ (x \ y y \ x) = z x y z \ x z \ 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 α] :
    (x y) \ z = x \ z y \ z
    theorem inf_sdiff_assoc {α : Type u} {x : α} {y : α} {z : α} [GeneralizedBooleanAlgebra α] :
    (x y) \ z = x y \ z
    theorem inf_sdiff_right_comm {α : Type u} {x : α} {y : α} {z : α} [GeneralizedBooleanAlgebra α] :
    x \ z y = (x y) \ z
    theorem inf_sdiff_distrib_left {α : Type u} [GeneralizedBooleanAlgebra α] (a : α) (b : α) (c : α) :
    a b \ c = (a b) \ (a c)
    theorem inf_sdiff_distrib_right {α : Type u} [GeneralizedBooleanAlgebra α] (a : α) (b : α) (c : α) :
    a \ b c = (a c) \ (b c)
    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 α] :
    x y = x \ y y \ x x y
    theorem sup_lt_of_lt_sdiff_left {α : Type u} {x : α} {y : α} {z : α} [GeneralizedBooleanAlgebra α] (h : y < z \ x) (hxz : x z) :
    x y < z
    theorem sup_lt_of_lt_sdiff_right {α : Type u} {x : α} {y : α} {z : α} [GeneralizedBooleanAlgebra α] (h : x < z \ y) (hyz : y z) :
    x y < z
    Equations
    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.

    • sup : ααα
    • le : ααProp
    • lt : ααProp
    • le_refl : ∀ (a : α), a a
    • le_trans : ∀ (a b c : α), a bb ca c
    • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
    • le_antisymm : ∀ (a b : α), a bb aa = b
    • le_sup_left : ∀ (a b : α), a a b
    • le_sup_right : ∀ (a b : α), b a b
    • sup_le : ∀ (a b c : α), a cb ca b c
    • inf : ααα
    • inf_le_left : ∀ (a b : α), a b a
    • inf_le_right : ∀ (a b : α), a b b
    • le_inf : ∀ (a b c : α), a ba ca b c
    • le_sup_inf : ∀ (x y z : α), (x y) (x z) x y z
    • compl : αα
    • sdiff : ααα
    • himp : ααα
    • top : α
    • bot : α
    • inf_compl_le_bot : ∀ (x : α), x x

      The infimum of x and xᶜ is at most

    • top_le_sup_compl : ∀ (x : α), x x

      The supremum of x and xᶜ is at least

    • le_top : ∀ (a : α), a

      is the greatest element

    • bot_le : ∀ (a : α), a

      is the least element

    • sdiff_eq : ∀ (x y : α), x \ y = x y

      x \ y is equal to x ⊓ yᶜ

    • himp_eq : ∀ (x y : α), x y = y x

      x ⇨ y is equal to y ⊔ xᶜ

    Instances
      Equations
      • BooleanAlgebra.toBoundedOrder = BoundedOrder.mk
      @[reducible]

      A bounded generalized boolean algebra is a boolean algebra.

      Equations
      • GeneralizedBooleanAlgebra.toBooleanAlgebra = let __spread.0 := inst✝; let __spread.1 := GeneralizedBooleanAlgebra.toOrderBot; let __spread.2 := inst; BooleanAlgebra.mk
      Instances For
        theorem inf_compl_eq_bot' {α : Type u} {x : α} [BooleanAlgebra α] :
        @[simp]
        theorem sup_compl_eq_top {α : Type u} {x : α} [BooleanAlgebra α] :
        @[simp]
        theorem compl_sup_eq_top {α : Type u} {x : α} [BooleanAlgebra α] :
        theorem isCompl_compl {α : Type u} {x : α} [BooleanAlgebra α] :
        theorem sdiff_eq {α : Type u} {x : α} {y : α} [BooleanAlgebra α] :
        x \ y = x y
        theorem himp_eq {α : Type u} {x : α} {y : α} [BooleanAlgebra α] :
        x y = y x
        Equations
        Equations
        • BooleanAlgebra.toBiheytingAlgebra = let __spread.0 := inst; let __spread.1 := GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra; BiheytingAlgebra.mk
        @[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 : α) :
        theorem compl_comp_compl {α : Type u} [BooleanAlgebra α] :
        compl compl = id
        @[simp]
        @[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 α] :
        (x y) = x y
        @[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 = x y
        Equations
        @[simp]
        theorem sup_inf_inf_compl {α : Type u} {x : α} {y : α} [BooleanAlgebra α] :
        x y x y = x
        @[simp]
        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_iff {α : 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
        Equations
        • One or more equations did not get rendered due to their size.
        instance Prod.instBooleanAlgebra (α : Type u_2) (β : Type u_3) [BooleanAlgebra α] [BooleanAlgebra β] :
        Equations
        instance Pi.instBooleanAlgebra {ι : Type u} {α : ιType v} [(i : ι) → BooleanAlgebra (α i)] :
        BooleanAlgebra ((i : ι) → α i)
        Equations
        • Pi.instBooleanAlgebra = let __spread.0 := Pi.sdiff; let __spread.1 := Pi.instHeytingAlgebra; let __spread.2 := Pi.instDistribLattice; BooleanAlgebra.mk
        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem Bool.sup_eq_bor :
        (fun (x x_1 : Bool) => x x_1) = or
        @[simp]
        theorem Bool.inf_eq_band :
        (fun (x x_1 : Bool) => x x_1) = and
        @[simp]
        theorem Bool.compl_eq_bnot :
        compl = not
        @[reducible]
        def Function.Injective.generalizedBooleanAlgebra {α : Type u} {β : Type u_1} [Sup α] [Inf α] [Bot α] [SDiff α] [GeneralizedBooleanAlgebra β] (f : αβ) (hf : Function.Injective f) (map_sup : ∀ (a b : α), f (a b) = f a f b) (map_inf : ∀ (a b : α), f (a b) = f a f b) (map_bot : f = ) (map_sdiff : ∀ (a b : α), f (a \ b) = f a \ f b) :

        Pullback a GeneralizedBooleanAlgebra along an injection.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[reducible]
          def Function.Injective.booleanAlgebra {α : Type u} {β : Type u_1} [Sup α] [Inf α] [Top α] [Bot α] [HasCompl α] [SDiff α] [BooleanAlgebra β] (f : αβ) (hf : Function.Injective f) (map_sup : ∀ (a b : α), f (a b) = f a f b) (map_inf : ∀ (a b : α), f (a b) = f a f 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) :

          Pullback a BooleanAlgebra along an injection.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.