doc-next-gen

Mathlib.Order.BooleanAlgebra

Module docstring

{"# (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

  • GeneralizedBooleanAlgebra: a type class for generalized Boolean algebras
  • BooleanAlgebra: a type class for Boolean algebras.
  • Prop.booleanAlgebra: the Boolean algebra instance on Prop

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:

","### Boolean algebras "}

GeneralizedBooleanAlgebra structure
(α : Type u) extends DistribLattice α, SDiff α, Bot α
Full source 
/-- 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`) `α`. -/
class GeneralizedBooleanAlgebra (α : Type u) extends DistribLattice α, SDiff α, Bot α where
  /-- For any `a`, `b`, `(a ⊓ b) ⊔ (a / b) = a` -/
  sup_inf_sdiff : ∀ a b : α, a ⊓ ba ⊓ b ⊔ a \ b = a
  /-- For any `a`, `b`, `(a ⊓ b) ⊓ (a / b) = ⊥` -/
  inf_inf_sdiff : ∀ a b : α, a ⊓ ba ⊓ b ⊓ a \ b = ⊥
Generalized Boolean Algebra
Informal description
A generalized Boolean algebra is a distributive lattice with a bottom element $\bot$ and a relative complement operation $\setminus$ (called `sdiff`) satisfying the following properties for all elements $x, y$: 1. $(x \sqcap y) \sqcup (x \setminus y) = x$ 2. $(x \sqcap y) \sqcap (x \setminus y) = \bot$ This structure generalizes Boolean algebras by not requiring a top element or global complements, making it applicable to settings like the lattice of finite subsets of an arbitrary type.
sup_inf_sdiff theorem
(x y : α) : x ⊓ y ⊔ x \ y = x
Full source 
@[simp]
theorem sup_inf_sdiff (x y : α) : x ⊓ yx ⊓ y ⊔ x \ y = x :=
  GeneralizedBooleanAlgebra.sup_inf_sdiff _ _
Join of Meet and Relative Complement Equals Original Element
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra $\alpha$, the join of the meet $x \sqcap y$ and the relative complement $x \setminus y$ equals $x$, i.e., $(x \sqcap y) \sqcup (x \setminus y) = x$.
inf_inf_sdiff theorem
(x y : α) : x ⊓ y ⊓ x \ y = ⊥
Full source 
@[simp]
theorem inf_inf_sdiff (x y : α) : x ⊓ yx ⊓ y ⊓ x \ y = ⊥ :=
  GeneralizedBooleanAlgebra.inf_inf_sdiff _ _
Relative Complement and Meet Annihilate to Bottom
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra $\alpha$, the meet of $x \sqcap y$ and the relative complement $x \setminus y$ is equal to the bottom element $\bot$, i.e., $(x \sqcap y) \sqcap (x \setminus y) = \bot$.
sup_sdiff_inf theorem
(x y : α) : x \ y ⊔ x ⊓ y = x
Full source 
@[simp]
theorem sup_sdiff_inf (x y : α) : x \ yx \ y ⊔ x ⊓ y = x := by rw [sup_comm, sup_inf_sdiff]
Join of Relative Complement and Meet Equals Original Element
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra $\alpha$, the join of the relative complement $x \setminus y$ and the meet $x \sqcap y$ equals $x$, i.e., $(x \setminus y) \sqcup (x \sqcap y) = x$.
inf_sdiff_inf theorem
(x y : α) : x \ y ⊓ (x ⊓ y) = ⊥
Full source 
@[simp]
theorem inf_sdiff_inf (x y : α) : x \ yx \ y ⊓ (x ⊓ y) = ⊥ := by rw [inf_comm, inf_inf_sdiff]
Annihilation of Relative Complement and Meet by Bottom Element
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra $\alpha$, the meet of the relative complement $x \setminus y$ and the meet $x \sqcap y$ is equal to the bottom element $\bot$, i.e., $(x \setminus y) \sqcap (x \sqcap y) = \bot$.
disjoint_inf_sdiff theorem
: Disjoint (x ⊓ y) (x \ y)
Full source 
theorem disjoint_inf_sdiff : Disjoint (x ⊓ y) (x \ y) :=
  disjoint_iff_inf_le.mpr (inf_inf_sdiff x y).le
Disjointness of Meet and Relative Complement: $x \sqcap y \perp x \setminus y$
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra, the meet $x \sqcap y$ is disjoint from the relative complement $x \setminus y$.
sdiff_unique theorem
(s : x ⊓ y ⊔ z = x) (i : x ⊓ y ⊓ z = ⊥) : x \ y = z
Full source 
theorem sdiff_unique (s : x ⊓ yx ⊓ y ⊔ z = x) (i : x ⊓ yx ⊓ y ⊓ z = ⊥) : x \ y = z := by
  conv_rhs at s => rw [← sup_inf_sdiff x y, sup_comm]
  rw [sup_comm] at s
  conv_rhs at i => rw [← inf_inf_sdiff x y, inf_comm]
  rw [inf_comm] at i
  exact (eq_of_inf_eq_sup_eq i s).symm
Uniqueness of Relative Complement in Generalized Boolean Algebras
Informal description
Let $\alpha$ be a generalized Boolean algebra, and let $x, y, z \in \alpha$ be elements such that: 1. $(x \sqcap y) \sqcup z = x$ (sup condition) 2. $(x \sqcap y) \sqcap z = \bot$ (inf condition) Then the relative complement of $y$ in $x$ is uniquely determined as $x \setminus y = z$.
sdiff_inf_sdiff theorem
: x \ y ⊓ y \ x = ⊥
Full source 
@[simp]
theorem sdiff_inf_sdiff : x \ yx \ y ⊓ y \ x = ⊥ :=
  Eq.symm <|
    calc
      ⊥ = x ⊓ yx ⊓ y ⊓ x \ y := by rw [inf_inf_sdiff]
      _ = x ⊓ (y ⊓ x ⊔ y \ x)x ⊓ (y ⊓ x ⊔ y \ x) ⊓ x \ y := by rw [sup_inf_sdiff]
      _ = (x ⊓ (y ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y := by rw [inf_sup_left]
      _ = (y ⊓ (x ⊓ x) ⊔ x ⊓ y \ x) ⊓ x \ y := by ac_rfl
      _ = (y ⊓ x ⊔ x ⊓ y \ x) ⊓ x \ y := by rw [inf_idem]
      _ = x ⊓ yx ⊓ y ⊓ x \ yx ⊓ y ⊓ x \ y ⊔ x ⊓ y \ x ⊓ x \ y := by rw [inf_sup_right, inf_comm x y]
      _ = x ⊓ y \ xx ⊓ y \ x ⊓ x \ y := by rw [inf_inf_sdiff, bot_sup_eq]
      _ = x ⊓ x \ yx ⊓ x \ y ⊓ y \ x := by ac_rfl
      _ = x \ yx \ y ⊓ y \ x := by rw [inf_of_le_right sdiff_le']
Relative Complements Annihilate Each Other: $(x \setminus y) \sqcap (y \setminus x) = \bot$
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra, the meet of the relative complements $x \setminus y$ and $y \setminus x$ is equal to the bottom element $\bot$, i.e., $(x \setminus y) \sqcap (y \setminus x) = \bot$.
disjoint_sdiff_sdiff theorem
: Disjoint (x \ y) (y \ x)
Full source 
theorem disjoint_sdiff_sdiff : Disjoint (x \ y) (y \ x) :=
  disjoint_iff_inf_le.mpr sdiff_inf_sdiff.le
Disjointness of Relative Complements: $(x \setminus y) \sqcap (y \setminus x) = \bot$
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra, the relative complements $x \setminus y$ and $y \setminus x$ are disjoint, i.e., $(x \setminus y) \sqcap (y \setminus x) = \bot$.
inf_sdiff_self_right theorem
: x ⊓ y \ x = ⊥
Full source 
@[simp]
theorem inf_sdiff_self_right : x ⊓ y \ x = ⊥ :=
  calc
    x ⊓ y \ x = (x ⊓ y ⊔ x \ y) ⊓ y \ x := by rw [sup_inf_sdiff]
    _ = x ⊓ yx ⊓ y ⊓ y \ xx ⊓ y ⊓ y \ x ⊔ x \ y ⊓ y \ x := by rw [inf_sup_right]
    _ = ⊥ := by rw [inf_comm x y, inf_inf_sdiff, sdiff_inf_sdiff, bot_sup_eq]
Annihilation of Meet with Relative Complement: $x \sqcap (y \setminus x) = \bot$
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra, the meet of $x$ and the relative complement $y \setminus x$ is equal to the bottom element $\bot$, i.e., $x \sqcap (y \setminus x) = \bot$.
inf_sdiff_self_left theorem
: y \ x ⊓ x = ⊥
Full source 
@[simp]
theorem inf_sdiff_self_left : y \ xy \ x ⊓ x = ⊥ := by rw [inf_comm, inf_sdiff_self_right]
Annihilation of Relative Complement with Meet: $(y \setminus x) \sqcap x = \bot$
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra, the meet of the relative complement $y \setminus x$ and $x$ is equal to the bottom element $\bot$, i.e., $(y \setminus x) \sqcap x = \bot$.
GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra instance
: GeneralizedCoheytingAlgebra α
Full source 
instance (priority := 100) GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra :
    GeneralizedCoheytingAlgebra α where
  __ := ‹GeneralizedBooleanAlgebra α›
  __ := GeneralizedBooleanAlgebra.toOrderBot
  sdiff := (· \ ·)
  sdiff_le_iff y x z :=
    ⟨fun h =>
      le_of_inf_le_sup_le
        (le_of_eq
          (calc
            y ⊓ y \ x = y \ x := inf_of_le_right sdiff_le'
            _ = x ⊓ y \ x ⊔ z ⊓ y \ x := by
              rw [inf_eq_right.2 h, inf_sdiff_self_right, bot_sup_eq]
            _ = (x ⊔ z) ⊓ y \ x := by rw [← inf_sup_right]))
        (calc
          y ⊔ y \ x = y := sup_of_le_left sdiff_le'
          _ ≤ y ⊔ (x ⊔ z) := le_sup_left
          _ = y \ x ⊔ x ⊔ z := by rw [← sup_assoc, ← @sdiff_sup_self' _ x y]
          _ = x ⊔ z ⊔ y \ x := by ac_rfl),
      fun h =>
      le_of_inf_le_sup_le
        (calc
          y \ x ⊓ x = ⊥ := inf_sdiff_self_left
          _ ≤ z ⊓ x := bot_le)
        (calc
          y \ x ⊔ x = y ⊔ x := sdiff_sup_self'
          _ ≤ x ⊔ z ⊔ x := sup_le_sup_right h x
          _ ≤ z ⊔ x := by rw [sup_assoc, sup_comm, sup_assoc, sup_idem])⟩
Generalized Boolean Algebras as Generalized Co-Heyting Algebras
Informal description
Every generalized Boolean algebra $\alpha$ is also a generalized co-Heyting algebra. This means that the relative complement operation $\setminus$ in the generalized Boolean algebra satisfies the adjunction property: for any elements $a, b, c \in \alpha$, we have $a \setminus b \leq c$ if and only if $a \leq b \sqcup c$.
disjoint_sdiff_self_left theorem
: Disjoint (y \ x) x
Full source 
theorem disjoint_sdiff_self_left : Disjoint (y \ x) x :=
  disjoint_iff_inf_le.mpr inf_sdiff_self_left.le
Disjointness of Relative Complement: $(y \setminus x) \perp x$
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra, the relative complement $y \setminus x$ is disjoint from $x$, i.e., $(y \setminus x) \sqcap x = \bot$.
disjoint_sdiff_self_right theorem
: Disjoint x (y \ x)
Full source 
theorem disjoint_sdiff_self_right : Disjoint x (y \ x) :=
  disjoint_iff_inf_le.mpr inf_sdiff_self_right.le
Disjointness of Element with Its Relative Complement: $x \perp (y \setminus x)$
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra, the element $x$ is disjoint from the relative complement $y \setminus x$, i.e., $x \sqcap (y \setminus x) = \bot$.
le_sdiff theorem
: x ≤ y \ z ↔ x ≤ y ∧ Disjoint x z
Full source 
lemma le_sdiff : x ≤ y \ z ↔ x ≤ y ∧ Disjoint x z :=
  ⟨fun h ↦ ⟨h.trans sdiff_le, disjoint_sdiff_self_left.mono_left h⟩, fun h ↦
    by rw [← h.2.sdiff_eq_left]; exact sdiff_le_sdiff_right h.1⟩
Characterization of Order via Relative Complement and Disjointness: $x \leq y \setminus z \leftrightarrow (x \leq y \land x \perp z)$
Informal description
For any elements $x, y, z$ in a generalized Boolean algebra, $x$ is less than or equal to the relative complement $y \setminus z$ if and only if $x$ is less than or equal to $y$ and $x$ is disjoint from $z$.
sdiff_eq_left theorem
: x \ y = x ↔ Disjoint x y
Full source 
@[simp] lemma sdiff_eq_left : x \ yx \ y = x ↔ Disjoint x y :=
  ⟨fun h ↦ disjoint_sdiff_self_left.mono_left h.ge, Disjoint.sdiff_eq_left⟩
Relative Complement Equals Original Element if and only if Disjoint: $x \setminus y = x \leftrightarrow x \perp y$
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra, the relative complement $x \setminus y$ equals $x$ if and only if $x$ and $y$ are disjoint (i.e., $x \sqcap y = \bot$).
Disjoint.sdiff_eq_of_sup_eq theorem
(hi : Disjoint x z) (hs : x ⊔ z = y) : y \ x = z
Full source 
theorem Disjoint.sdiff_eq_of_sup_eq (hi : Disjoint x z) (hs : x ⊔ z = y) : y \ x = z :=
  have h : y ⊓ x = x := inf_eq_right.2 <| le_sup_left.trans hs.le
  sdiff_unique (by rw [h, hs]) (by rw [h, hi.eq_bot])
Relative Complement Characterization via Disjointness and Supremum
Informal description
Let $\alpha$ be a generalized Boolean algebra, and let $x, y, z \in \alpha$ be elements such that: 1. $x$ and $z$ are disjoint (i.e., $x \sqcap z = \bot$) 2. The supremum of $x$ and $z$ equals $y$ (i.e., $x \sqcup z = y$) Then the relative complement of $x$ in $y$ is equal to $z$, i.e., $y \setminus x = z$.
Disjoint.sdiff_unique theorem
(hd : Disjoint x z) (hz : z ≤ y) (hs : y ≤ x ⊔ z) : y \ x = z
Full source 
protected theorem Disjoint.sdiff_unique (hd : Disjoint x z) (hz : z ≤ y) (hs : y ≤ x ⊔ z) :
    y \ x = z :=
  sdiff_unique
    (by
      rw [← inf_eq_right] at hs
      rwa [sup_inf_right, inf_sup_right, sup_comm x, inf_sup_self, inf_comm, sup_comm z,
        hs, sup_eq_left])
    (by rw [inf_assoc, hd.eq_bot, inf_bot_eq])
Uniqueness of Relative Complement under Disjointness and Bounds
Informal description
Let $\alpha$ be a generalized Boolean algebra, and let $x, y, z \in \alpha$ be elements such that: 1. $x$ and $z$ are disjoint (i.e., $x \sqcap z = \bot$), 2. $z \leq y$, 3. $y \leq x \sqcup z$. Then the relative complement of $x$ in $y$ is uniquely determined as $y \setminus x = z$.
disjoint_sdiff_iff_le theorem
(hz : z ≤ y) (hx : x ≤ y) : Disjoint z (y \ x) ↔ z ≤ x
Full source 
theorem disjoint_sdiff_iff_le (hz : z ≤ y) (hx : x ≤ y) : DisjointDisjoint z (y \ x) ↔ z ≤ x :=
  ⟨fun H =>
    le_of_inf_le_sup_le (le_trans H.le_bot bot_le)
      (by
        rw [sup_sdiff_cancel_right hx]
        refine le_trans (sup_le_sup_left sdiff_le z) ?_
        rw [sup_eq_right.2 hz]),
    fun H => disjoint_sdiff_self_right.mono_left H⟩
Disjointness of Element with Relative Complement is Equivalent to Order Relation: $z \perp (y \setminus x) \leftrightarrow z \leq x$
Informal description
Let $\alpha$ be a generalized Boolean algebra, and let $x, y, z \in \alpha$ be elements such that $z \leq y$ and $x \leq y$. Then $z$ is disjoint from the relative complement $y \setminus x$ if and only if $z \leq x$. In other words, $z \sqcap (y \setminus x) = \bot$ if and only if $z \leq x$.
le_iff_disjoint_sdiff theorem
(hz : z ≤ y) (hx : x ≤ y) : z ≤ x ↔ Disjoint z (y \ x)
Full source 
theorem le_iff_disjoint_sdiff (hz : z ≤ y) (hx : x ≤ y) : z ≤ x ↔ Disjoint z (y \ x) :=
  (disjoint_sdiff_iff_le hz hx).symm
Order Relation via Disjointness with Relative Complement: $z \leq x \leftrightarrow z \perp (y \setminus x)$ under $z, x \leq y$
Informal description
Let $\alpha$ be a generalized Boolean algebra, and let $x, y, z \in \alpha$ be elements such that $z \leq y$ and $x \leq y$. Then $z \leq x$ if and only if $z$ is disjoint from the relative complement $y \setminus x$, i.e., $z \sqcap (y \setminus x) = \bot$.
inf_sdiff_eq_bot_iff theorem
(hz : z ≤ y) (hx : x ≤ y) : z ⊓ y \ x = ⊥ ↔ z ≤ x
Full source 
theorem inf_sdiff_eq_bot_iff (hz : z ≤ y) (hx : x ≤ y) : z ⊓ y \ xz ⊓ y \ x = ⊥ ↔ z ≤ x := by
  rw [← disjoint_iff]
  exact disjoint_sdiff_iff_le hz hx
Infimum with Relative Complement is Bottom iff Order Relation Holds: $z \sqcap (y \setminus x) = \bot \leftrightarrow z \leq x$
Informal description
Let $\alpha$ be a generalized Boolean algebra, and let $x, y, z \in \alpha$ be elements such that $z \leq y$ and $x \leq y$. Then the infimum of $z$ and the relative complement $y \setminus x$ equals the bottom element $\bot$ if and only if $z \leq x$. In other words, $$ z \sqcap (y \setminus x) = \bot \leftrightarrow z \leq x. $$
le_iff_eq_sup_sdiff theorem
(hz : z ≤ y) (hx : x ≤ y) : x ≤ z ↔ y = z ⊔ y \ x
Full source 
theorem le_iff_eq_sup_sdiff (hz : z ≤ y) (hx : x ≤ y) : x ≤ z ↔ y = z ⊔ y \ x :=
  ⟨fun H => by
    apply le_antisymm
    · conv_lhs => rw [← sup_inf_sdiff y x]
      apply sup_le_sup_right
      rwa [inf_eq_right.2 hx]
    · apply le_trans
      · apply sup_le_sup_right hz
      · rw [sup_sdiff_left],
    fun H => by
    conv_lhs at H => rw [← sup_sdiff_cancel_right hx]
    refine le_of_inf_le_sup_le ?_ H.le
    rw [inf_sdiff_self_right]
    exact bot_le⟩
Characterization of Order via Join and Relative Complement: $x \leq z \iff y = z \sqcup (y \setminus x)$ under $z, x \leq y$
Informal description
For any elements $x, y, z$ in a generalized Boolean algebra such that $z \leq y$ and $x \leq y$, the inequality $x \leq z$ holds if and only if $y$ is equal to the join of $z$ and the relative complement $y \setminus x$.
sdiff_sup theorem
: y \ (x ⊔ z) = y \ x ⊓ y \ z
Full source 
theorem sdiff_sup : y \ (x ⊔ z) = y \ xy \ x ⊓ y \ z :=
  sdiff_unique
    (calc
      y ⊓ (x ⊔ z)y ⊓ (x ⊔ z) ⊔ y \ x ⊓ y \ z = (y ⊓ (x ⊔ z) ⊔ y \ x) ⊓ (y ⊓ (x ⊔ z) ⊔ y \ z) := by
          rw [sup_inf_left]
      _ = (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z) := by rw [@inf_sup_left _ _ y]
      _ = (y ⊓ z ⊔ (y ⊓ x ⊔ y \ x)) ⊓ (y ⊓ x ⊔ (y ⊓ z ⊔ y \ z)) := by ac_rfl
      _ = (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y) := by rw [sup_inf_sdiff, sup_inf_sdiff]
      _ = (y ⊔ y ⊓ z) ⊓ (y ⊔ y ⊓ x) := by ac_rfl
      _ = y := by rw [sup_inf_self, sup_inf_self, inf_idem])
    (calc
      y ⊓ (x ⊔ z)y ⊓ (x ⊔ z) ⊓ (y \ x ⊓ y \ z) = (y ⊓ x ⊔ y ⊓ z) ⊓ (y \ x ⊓ y \ z) := by rw [inf_sup_left]
      _ = y ⊓ xy ⊓ x ⊓ (y \ x ⊓ y \ z)y ⊓ x ⊓ (y \ x ⊓ y \ z) ⊔ y ⊓ z ⊓ (y \ x ⊓ y \ z) := by rw [inf_sup_right]
      _ = y ⊓ xy ⊓ x ⊓ y \ xy ⊓ x ⊓ y \ x ⊓ y \ zy ⊓ x ⊓ y \ x ⊓ y \ z ⊔ y \ x ⊓ (y \ z ⊓ (y ⊓ z)) := by ac_rfl
      _ = ⊥ := by rw [inf_inf_sdiff, bot_inf_eq, bot_sup_eq, inf_comm (y \ z),
                      inf_inf_sdiff, inf_bot_eq])
Relative Complement Distributes over Join via Meet: $y \setminus (x \sqcup z) = (y \setminus x) \sqcap (y \setminus z)$
Informal description
For any elements $x, y, z$ in a generalized Boolean algebra, the relative complement of $x \sqcup z$ in $y$ equals the meet of the relative complements of $x$ in $y$ and $z$ in $y$, i.e., $$ y \setminus (x \sqcup z) = (y \setminus x) \sqcap (y \setminus z). $$
sdiff_eq_sdiff_iff_inf_eq_inf theorem
: y \ x = y \ z ↔ y ⊓ x = y ⊓ z
Full source 
theorem sdiff_eq_sdiff_iff_inf_eq_inf : y \ xy \ x = y \ z ↔ y ⊓ x = y ⊓ z :=
  ⟨fun h => eq_of_inf_eq_sup_eq (a := y \ x) (by rw [inf_inf_sdiff, h, inf_inf_sdiff])
    (by rw [sup_inf_sdiff, h, sup_inf_sdiff]),
    fun h => by rw [← sdiff_inf_self_right, ← sdiff_inf_self_right z y, inf_comm, h, inf_comm]⟩
Relative Complement Equality Condition via Meet Equality: $y \setminus x = y \setminus z \iff y \sqcap x = y \sqcap z$
Informal description
For any elements $x, y, z$ in a generalized Boolean algebra, the relative complements $y \setminus x$ and $y \setminus z$ are equal if and only if the meets $y \sqcap x$ and $y \sqcap z$ are equal. That is, $$ y \setminus x = y \setminus z \iff y \sqcap x = y \sqcap z. $$
sdiff_eq_self_iff_disjoint theorem
: x \ y = x ↔ Disjoint y x
Full source 
theorem sdiff_eq_self_iff_disjoint : x \ yx \ y = x ↔ Disjoint y x :=
  calc
    x \ y = x ↔ x \ y = x \ ⊥ := by rw [sdiff_bot]
    _ ↔ x ⊓ y = x ⊓ ⊥calc
    x \ y = x ↔ x \ y = x \ ⊥ := by rw [sdiff_bot]
    _ ↔ x ⊓ y = x ⊓ ⊥ := sdiff_eq_sdiff_iff_inf_eq_inf
    _ ↔ Disjoint y x := by rw [inf_bot_eq, inf_comm, disjoint_iff]
Relative Complement Equals Original Element if and only if Elements are Disjoint: $x \setminus y = x \iff y \sqcap x = \bot$
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra, the relative complement $x \setminus y$ equals $x$ if and only if $y$ and $x$ are disjoint (i.e., $y \sqcap x = \bot$).
sdiff_eq_self_iff_disjoint' theorem
: x \ y = x ↔ Disjoint x y
Full source 
theorem sdiff_eq_self_iff_disjoint' : x \ yx \ y = x ↔ Disjoint x y := by
  rw [sdiff_eq_self_iff_disjoint, disjoint_comm]
Relative complement equals original element if and only if elements are disjoint: $x \setminus y = x \iff x \sqcap y = \bot$
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra, the relative complement $x \setminus y$ equals $x$ if and only if $x$ and $y$ are disjoint (i.e., $x \sqcap y = \bot$).
sdiff_lt theorem
(hx : y ≤ x) (hy : y ≠ ⊥) : x \ y < x
Full source 
theorem sdiff_lt (hx : y ≤ x) (hy : y ≠ ⊥) : x \ y < x := by
  refine sdiff_le.lt_of_ne fun h => hy ?_
  rw [sdiff_eq_self_iff_disjoint', disjoint_iff] at h
  rw [← h, inf_eq_right.mpr hx]
Strict Inequality for Relative Complement: $y \leq x \land y \neq \bot \implies x \setminus y < x$
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra, if $y \leq x$ and $y \neq \bot$, then the relative complement $x \setminus y$ is strictly less than $x$.
sdiff_lt_left theorem
: x \ y < x ↔ ¬Disjoint y x
Full source 
theorem sdiff_lt_left : x \ yx \ y < x ↔ ¬ Disjoint y x := by
  rw [lt_iff_le_and_ne, Ne, sdiff_eq_self_iff_disjoint, and_iff_right sdiff_le]
Relative Complement is Strictly Less Than Original if and only if Elements are Not Disjoint: $x \setminus y < x \iff y \sqcap x \neq \bot$
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra, the relative complement $x \setminus y$ is strictly less than $x$ if and only if $y$ and $x$ are not disjoint (i.e., $y \sqcap x \neq \bot$).
le_sdiff_right theorem
: x ≤ y \ x ↔ x = ⊥
Full source 
@[simp]
theorem le_sdiff_right : x ≤ y \ x ↔ x = ⊥ :=
  ⟨fun h => disjoint_self.1 (disjoint_sdiff_self_right.mono_right h), fun h => h.le.trans bot_le⟩
Characterization of Bottom Element via Relative Complement: $x \leq y \setminus x \iff x = \bot$
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra, $x$ is less than or equal to the relative complement $y \setminus x$ if and only if $x$ is the bottom element $\bot$.
sdiff_eq_right theorem
: x \ y = y ↔ x = ⊥ ∧ y = ⊥
Full source 
@[simp] lemma sdiff_eq_right : x \ yx \ y = y ↔ x = ⊥ ∧ y = ⊥ := by
  rw [disjoint_sdiff_self_left.eq_iff]; aesop
Characterization of Bottom Elements via Relative Complement: $x \setminus y = y \leftrightarrow x = \bot \land y = \bot$
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra, the relative complement $x \setminus y$ equals $y$ if and only if both $x$ and $y$ are equal to the bottom element $\bot$. That is, $x \setminus y = y \leftrightarrow x = \bot \land y = \bot$.
sdiff_ne_right theorem
: x \ y ≠ y ↔ x ≠ ⊥ ∨ y ≠ ⊥
Full source 
lemma sdiff_ne_right : x \ yx \ y ≠ yx \ y ≠ y ↔ x ≠ ⊥ ∨ y ≠ ⊥ := sdiff_eq_right.not.trans not_and_or
Non-Equality Characterization via Relative Complement: $x \setminus y \neq y \leftrightarrow x \neq \bot \lor y \neq \bot$
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra, the relative complement $x \setminus y$ is not equal to $y$ if and only if either $x$ is not the bottom element $\bot$ or $y$ is not the bottom element $\bot$. That is, $x \setminus y \neq y \leftrightarrow x \neq \bot \lor y \neq \bot$.
sdiff_lt_sdiff_right theorem
(h : x < y) (hz : z ≤ x) : x \ z < y \ z
Full source 
theorem sdiff_lt_sdiff_right (h : x < y) (hz : z ≤ x) : x \ z < y \ z :=
  (sdiff_le_sdiff_right h.le).lt_of_not_le
    fun h' => h.not_le <| le_sdiff_sup.trans <| sup_le_of_le_sdiff_right h' hz
Strict Monotonicity of Relative Complement: $x < y \Rightarrow x \setminus z < y \setminus z$ when $z \leq x$
Informal description
In a generalized Boolean algebra, if $x < y$ and $z \leq x$, then the relative complement $x \setminus z$ is strictly less than the relative complement $y \setminus z$.
sup_inf_inf_sdiff theorem
: x ⊓ y ⊓ z ⊔ y \ z = x ⊓ y ⊔ y \ z
Full source 
theorem sup_inf_inf_sdiff : x ⊓ yx ⊓ y ⊓ zx ⊓ y ⊓ z ⊔ y \ z = x ⊓ yx ⊓ y ⊔ y \ z :=
  calc
    x ⊓ yx ⊓ y ⊓ zx ⊓ y ⊓ z ⊔ y \ z = x ⊓ (y ⊓ z)x ⊓ (y ⊓ z) ⊔ y \ z := by rw [inf_assoc]
    _ = (x ⊔ y \ z) ⊓ y := by rw [sup_inf_right, sup_inf_sdiff]
    _ = x ⊓ yx ⊓ y ⊔ y \ z := by rw [inf_sup_right, inf_sdiff_left]
Join-Meet-Sdiff Identity in Generalized Boolean Algebras
Informal description
In a generalized Boolean algebra, for any elements $x, y, z$, the following equality holds: $$ (x \sqcap y \sqcap z) \sqcup (y \setminus z) = (x \sqcap y) \sqcup (y \setminus z). $$
sdiff_sdiff_right theorem
: x \ (y \ z) = x \ y ⊔ x ⊓ y ⊓ z
Full source 
theorem sdiff_sdiff_right : x \ (y \ z) = x \ yx \ y ⊔ x ⊓ y ⊓ z := by
  rw [sup_comm, inf_comm, ← inf_assoc, sup_inf_inf_sdiff]
  apply sdiff_unique
  · calc
      x ⊓ y \ zx ⊓ y \ z ⊔ (z ⊓ x ⊔ x \ y) = (x ⊔ (z ⊓ x ⊔ x \ y)) ⊓ (y \ z ⊔ (z ⊓ x ⊔ x \ y)) := by
          rw [sup_inf_right]
      _ = (x ⊔ x ⊓ z ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) := by ac_rfl
      _ = x ⊓ (y \ z ⊔ x ⊓ z ⊔ x \ y) := by rw [sup_inf_self, sup_sdiff_left, ← sup_assoc]
      _ = x ⊓ (y \ z ⊓ (z ⊔ y) ⊔ x ⊓ (z ⊔ y) ⊔ x \ y) := by
          rw [sup_inf_left, sdiff_sup_self', inf_sup_right, sup_comm y]
      _ = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y) := by
          rw [inf_sdiff_sup_right, @inf_sup_left _ _ x z y]
      _ = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ (x ⊓ y ⊔ x \ y))) := by ac_rfl
      _ = x ⊓ (y \ z ⊔ (x ⊔ x ⊓ z)) := by rw [sup_inf_sdiff, sup_comm (x ⊓ z)]
      _ = x := by rw [sup_inf_self, sup_comm, inf_sup_self]
  · calc
      x ⊓ y \ zx ⊓ y \ z ⊓ (z ⊓ x ⊔ x \ y) = x ⊓ y \ zx ⊓ y \ z ⊓ (z ⊓ x)x ⊓ y \ z ⊓ (z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y := by rw [inf_sup_left]
      _ = x ⊓ (y \ z ⊓ z ⊓ x)x ⊓ (y \ z ⊓ z ⊓ x) ⊔ x ⊓ y \ z ⊓ x \ y := by ac_rfl
      _ = x ⊓ y \ zx ⊓ y \ z ⊓ x \ y := by rw [inf_sdiff_self_left, bot_inf_eq, inf_bot_eq, bot_sup_eq]
      _ = x ⊓ (y \ z ⊓ y)x ⊓ (y \ z ⊓ y) ⊓ x \ y := by conv_lhs => rw [← inf_sdiff_left]
      _ = x ⊓ (y \ z ⊓ (y ⊓ x \ y)) := by ac_rfl
      _ = ⊥ := by rw [inf_sdiff_self_right, inf_bot_eq, inf_bot_eq]
Double Relative Complement Identity: $x \setminus (y \setminus z) = (x \setminus y) \sqcup (x \sqcap y \sqcap z)$
Informal description
For any elements $x, y, z$ in a generalized Boolean algebra, the relative complement of $x$ with respect to the relative complement of $y$ with respect to $z$ equals the join of the relative complement of $x$ with respect to $y$ and the meet of $x$, $y$, and $z$: $$ x \setminus (y \setminus z) = (x \setminus y) \sqcup (x \sqcap y \sqcap z). $$
sdiff_sdiff_right' theorem
: x \ (y \ z) = x \ y ⊔ x ⊓ z
Full source 
theorem sdiff_sdiff_right' : x \ (y \ z) = x \ yx \ y ⊔ x ⊓ z :=
  calc
    x \ (y \ z) = x \ yx \ y ⊔ x ⊓ y ⊓ z := sdiff_sdiff_right
    _ = z ⊓ xz ⊓ x ⊓ yz ⊓ x ⊓ y ⊔ x \ y := by ac_rfl
    _ = x \ yx \ y ⊔ x ⊓ z := by rw [sup_inf_inf_sdiff, sup_comm, inf_comm]
Simplified Double Relative Complement Identity: $x \setminus (y \setminus z) = (x \setminus y) \sqcup (x \sqcap z)$
Informal description
For any elements $x, y, z$ in a generalized Boolean algebra, the relative complement of $x$ with respect to the relative complement of $y$ with respect to $z$ equals the join of the relative complement of $x$ with respect to $y$ and the meet of $x$ and $z$: $$ x \setminus (y \setminus z) = (x \setminus y) \sqcup (x \sqcap z). $$
sdiff_sdiff_eq_sdiff_sup theorem
(h : z ≤ x) : x \ (y \ z) = x \ y ⊔ z
Full source 
theorem sdiff_sdiff_eq_sdiff_sup (h : z ≤ x) : x \ (y \ z) = x \ yx \ y ⊔ z := by
  rw [sdiff_sdiff_right', inf_eq_right.2 h]
Double Relative Complement Identity under Order Condition: $x \setminus (y \setminus z) = (x \setminus y) \sqcup z$ when $z \leq x$
Informal description
For any elements $x, y, z$ in a generalized Boolean algebra such that $z \leq x$, the relative complement of $x$ with respect to the relative complement of $y$ with respect to $z$ equals the join of the relative complement of $x$ with respect to $y$ and $z$, i.e., $$ x \setminus (y \setminus z) = (x \setminus y) \sqcup z. $$
sdiff_sdiff_right_self theorem
: x \ (x \ y) = x ⊓ y
Full source 
@[simp]
theorem sdiff_sdiff_right_self : x \ (x \ y) = x ⊓ y := by
  rw [sdiff_sdiff_right, inf_idem, sdiff_self, bot_sup_eq]
Double Relative Complement Identity: $x \setminus (x \setminus y) = x \sqcap y$
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra, the relative complement of $x$ with respect to the relative complement of $x$ with respect to $y$ equals the meet of $x$ and $y$, i.e., $$ x \setminus (x \setminus y) = x \sqcap y. $$
sdiff_sdiff_eq_self theorem
(h : y ≤ x) : x \ (x \ y) = y
Full source 
theorem sdiff_sdiff_eq_self (h : y ≤ x) : x \ (x \ y) = y := by
  rw [sdiff_sdiff_right_self, inf_of_le_right h]
Double Relative Complement Cancellation: $x \setminus (x \setminus y) = y$ when $y \leq x$
Informal description
For any elements $x$ and $y$ in a generalized Boolean algebra, if $y \leq x$, then the relative complement of $x$ with respect to the relative complement of $x$ with respect to $y$ equals $y$, i.e., $$ x \setminus (x \setminus y) = y. $$
sdiff_eq_symm theorem
(hy : y ≤ x) (h : x \ y = z) : x \ z = y
Full source 
theorem sdiff_eq_symm (hy : y ≤ x) (h : x \ y = z) : x \ z = y := by
  rw [← h, sdiff_sdiff_eq_self hy]
Symmetry of Relative Complement: $x \setminus y = z$ implies $x \setminus z = y$ when $y \leq x$
Informal description
For any elements $x, y, z$ in a generalized Boolean algebra, if $y \leq x$ and the relative complement of $x$ with respect to $y$ equals $z$, then the relative complement of $x$ with respect to $z$ equals $y$, i.e., $$ x \setminus z = y. $$
sdiff_eq_comm theorem
(hy : y ≤ x) (hz : z ≤ x) : x \ y = z ↔ x \ z = y
Full source 
theorem sdiff_eq_comm (hy : y ≤ x) (hz : z ≤ x) : x \ yx \ y = z ↔ x \ z = y :=
  ⟨sdiff_eq_symm hy, sdiff_eq_symm hz⟩
Commutativity of Relative Complement: $x \setminus y = z \leftrightarrow x \setminus z = y$ under $y, z \leq x$
Informal description
For any elements $x, y, z$ in a generalized Boolean algebra such that $y \leq x$ and $z \leq x$, the equality $x \setminus y = z$ holds if and only if $x \setminus z = y$.
sdiff_le_sdiff_iff_le theorem
(hx : x ≤ z) (hy : y ≤ z) : z \ x ≤ z \ y ↔ y ≤ x
Full source 
theorem sdiff_le_sdiff_iff_le (hx : x ≤ z) (hy : y ≤ z) : z \ xz \ x ≤ z \ y ↔ y ≤ x := by
  refine ⟨fun h ↦ ?_, sdiff_le_sdiff_left⟩
  rw [← sdiff_sdiff_eq_self hx, ← sdiff_sdiff_eq_self hy]
  exact sdiff_le_sdiff_left h
Relative Complement Order Reversal: $z \setminus x \leq z \setminus y \leftrightarrow y \leq x$ under $x, y \leq z$
Informal description
Let $x, y, z$ be elements of a generalized Boolean algebra such that $x \leq z$ and $y \leq z$. Then the relative complement $z \setminus x$ is less than or equal to $z \setminus y$ if and only if $y \leq x$.
sdiff_sdiff_left' theorem
: (x \ y) \ z = x \ y ⊓ x \ z
Full source 
theorem sdiff_sdiff_left' : (x \ y) \ z = x \ yx \ y ⊓ x \ z := by rw [sdiff_sdiff_left, sdiff_sup]
Double Relative Complement as Meet of Complements
Informal description
In a generalized Boolean algebra, for any elements $x, y, z$, the double relative complement $(x \setminus y) \setminus z$ equals the meet of the relative complements $x \setminus y$ and $x \setminus z$, i.e., $$ (x \setminus y) \setminus z = (x \setminus y) \sqcap (x \setminus z). $$
sdiff_sdiff_sup_sdiff theorem
: z \ (x \ y ⊔ y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x)
Full source 
theorem sdiff_sdiff_sup_sdiff : z \ (x \ y ⊔ y \ x) = z ⊓ (z \ x ⊔ y)z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x) :=
  calc
    z \ (x \ y ⊔ y \ x) = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) := by
        rw [sdiff_sup, sdiff_sdiff_right, sdiff_sdiff_right]
    _ = z ⊓ (z \ x ⊔ y)z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) := by rw [sup_inf_left, sup_comm, sup_inf_sdiff]
    _ = z ⊓ (z \ x ⊔ y)z ⊓ (z \ x ⊔ y) ⊓ (z ⊓ (z \ y ⊔ x)) := by
        rw [sup_inf_left, sup_comm (z \ y), sup_inf_sdiff]
    _ = z ⊓ zz ⊓ z ⊓ (z \ x ⊔ y)z ⊓ z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x) := by ac_rfl
    _ = z ⊓ (z \ x ⊔ y)z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x) := by rw [inf_idem]
Relative Complement of Symmetric Difference in Generalized Boolean Algebras: $z \setminus (x \setminus y \sqcup y \setminus x) = z \sqcap \big((z \setminus x \sqcup y) \sqcap (z \setminus y \sqcup x)\big)$
Informal description
For any elements $x, y, z$ in a generalized Boolean algebra, the relative complement of $z$ with respect to the symmetric difference $x \setminus y \sqcup y \setminus x$ equals the meet of $z$ with the two terms $(z \setminus x) \sqcup y$ and $(z \setminus y) \sqcup x$, i.e., $$ z \setminus (x \setminus y \sqcup y \setminus x) = z \sqcap \big((z \setminus x \sqcup y) \sqcap (z \setminus y \sqcup x)\big). $$
sdiff_sdiff_sup_sdiff' theorem
: z \ (x \ y ⊔ y \ x) = z ⊓ x ⊓ y ⊔ z \ x ⊓ z \ y
Full source 
theorem sdiff_sdiff_sup_sdiff' : z \ (x \ y ⊔ y \ x) = z ⊓ xz ⊓ x ⊓ yz ⊓ x ⊓ y ⊔ z \ x ⊓ z \ y :=
  calc
    z \ (x \ y ⊔ y \ x) = z \ (x \ y)z \ (x \ y) ⊓ z \ (y \ x) := sdiff_sup
    _ = (z \ x ⊔ z ⊓ x ⊓ y) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) := by rw [sdiff_sdiff_right, sdiff_sdiff_right]
    _ = (z \ x ⊔ z ⊓ y ⊓ x) ⊓ (z \ y ⊔ z ⊓ y ⊓ x) := by ac_rfl
    _ = z \ xz \ x ⊓ z \ yz \ x ⊓ z \ y ⊔ z ⊓ y ⊓ x := by rw [← sup_inf_right]
    _ = z ⊓ xz ⊓ x ⊓ yz ⊓ x ⊓ y ⊔ z \ x ⊓ z \ y := by ac_rfl
Relative Complement of Symmetric Difference: $z \setminus (x \setminus y \sqcup y \setminus x) = (z \sqcap x \sqcap y) \sqcup (z \setminus x \sqcap z \setminus y)$
Informal description
For any elements $x, y, z$ in a generalized Boolean algebra, the relative complement of $z$ with respect to the symmetric difference $x \setminus y \sqcup y \setminus x$ equals the join of the meet of $z$, $x$, and $y$ with the meet of the relative complements $z \setminus x$ and $z \setminus y$: $$ z \setminus (x \setminus y \sqcup y \setminus x) = (z \sqcap x \sqcap y) \sqcup (z \setminus x \sqcap z \setminus y). $$
sdiff_sdiff_sdiff_cancel_left theorem
(hca : z ≤ x) : (x \ y) \ (x \ z) = z \ y
Full source 
lemma sdiff_sdiff_sdiff_cancel_left (hca : z ≤ x) : (x \ y) \ (x \ z) = z \ y :=
  sdiff_sdiff_sdiff_le_sdiff.antisymm <|
    (disjoint_sdiff_self_right.mono_left sdiff_le).le_sdiff_of_le_left <| sdiff_le_sdiff_right hca
Relative Complement Cancellation: $(x \setminus y) \setminus (x \setminus z) = z \setminus y$ when $z \leq x$
Informal description
Let $\alpha$ be a generalized Boolean algebra. For any elements $x, y, z \in \alpha$ such that $z \leq x$, the following equality holds: $$(x \setminus y) \setminus (x \setminus z) = z \setminus y.$$
sdiff_sdiff_sdiff_cancel_right theorem
(hcb : z ≤ y) : (x \ z) \ (y \ z) = x \ y
Full source 
lemma sdiff_sdiff_sdiff_cancel_right (hcb : z ≤ y) : (x \ z) \ (y \ z) = x \ y := by
  rw [le_antisymm_iff, sdiff_le_comm]
  exact ⟨sdiff_sdiff_sdiff_le_sdiff,
    (disjoint_sdiff_self_left.mono_right sdiff_le).le_sdiff_of_le_left <| sdiff_le_sdiff_left hcb⟩
Relative Complement Cancellation: $(x \setminus z) \setminus (y \setminus z) = x \setminus y$ when $z \leq y$
Informal description
Let $\alpha$ be a generalized Boolean algebra. For any elements $x, y, z \in \alpha$ such that $z \leq y$, the following equality holds: $$(x \setminus z) \setminus (y \setminus z) = x \setminus y.$$
inf_sdiff theorem
: (x ⊓ y) \ z = x \ z ⊓ y \ z
Full source 
theorem inf_sdiff : (x ⊓ y) \ z = x \ zx \ z ⊓ y \ z :=
  sdiff_unique
    (calc
      x ⊓ yx ⊓ y ⊓ zx ⊓ y ⊓ z ⊔ x \ z ⊓ y \ z = (x ⊓ y ⊓ z ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) := by rw [sup_inf_left]
      _ = (x ⊓ y ⊓ (z ⊔ x) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) := by
          rw [sup_inf_right, sup_sdiff_self_right, inf_sup_right, inf_sdiff_sup_right]
      _ = (y ⊓ (x ⊓ (x ⊔ z)) ⊔ x \ z) ⊓ (x ⊓ y ⊓ z ⊔ y \ z) := by ac_rfl
      _ = (y ⊓ x ⊔ x \ z) ⊓ (x ⊓ y ⊔ y \ z) := by rw [inf_sup_self, sup_inf_inf_sdiff]
      _ = x ⊓ yx ⊓ y ⊔ x \ z ⊓ y \ z := by rw [inf_comm y, sup_inf_left]
      _ = x ⊓ y := sup_eq_left.2 (inf_le_inf sdiff_le sdiff_le))
    (calc
      x ⊓ yx ⊓ y ⊓ zx ⊓ y ⊓ z ⊓ (x \ z ⊓ y \ z) = x ⊓ yx ⊓ y ⊓ (z ⊓ x \ z)x ⊓ y ⊓ (z ⊓ x \ z) ⊓ y \ z := by ac_rfl
      _ = ⊥ := by rw [inf_sdiff_self_right, inf_bot_eq, bot_inf_eq])
Distributivity of Relative Complement over Meet: $(x \sqcap y) \setminus z = (x \setminus z) \sqcap (y \setminus z)$
Informal description
For any elements $x$, $y$, and $z$ in a generalized Boolean algebra $\alpha$, the relative complement of $z$ in the meet of $x$ and $y$ is equal to the meet of the relative complements of $z$ in $x$ and $z$ in $y$, i.e., $$ (x \sqcap y) \setminus z = (x \setminus z) \sqcap (y \setminus z). $$
inf_sdiff_assoc theorem
(x y z : α) : (x ⊓ y) \ z = x ⊓ y \ z
Full source 
/-- See also `sdiff_inf_right_comm`. -/
theorem inf_sdiff_assoc (x y z : α) : (x ⊓ y) \ z = x ⊓ y \ z :=
  sdiff_unique
    (calc
      x ⊓ yx ⊓ y ⊓ zx ⊓ y ⊓ z ⊔ x ⊓ y \ z = x ⊓ (y ⊓ z)x ⊓ (y ⊓ z) ⊔ x ⊓ y \ z := by rw [inf_assoc]
      _ = x ⊓ (y ⊓ z ⊔ y \ z) := by rw [← inf_sup_left]
      _ = x ⊓ y := by rw [sup_inf_sdiff])
    (calc
      x ⊓ yx ⊓ y ⊓ zx ⊓ y ⊓ z ⊓ (x ⊓ y \ z) = x ⊓ xx ⊓ x ⊓ (y ⊓ z ⊓ y \ z) := by ac_rfl
      _ = ⊥ := by rw [inf_inf_sdiff, inf_bot_eq])
Associativity of Meet with Relative Complement: $(x \sqcap y) \setminus z = x \sqcap (y \setminus z)$
Informal description
For any elements $x$, $y$, and $z$ in a generalized Boolean algebra $\alpha$, the relative complement of $z$ in the meet of $x$ and $y$ is equal to the meet of $x$ and the relative complement of $z$ in $y$. That is: $$ (x \sqcap y) \setminus z = x \sqcap (y \setminus z). $$
sdiff_inf_right_comm theorem
(x y z : α) : x \ z ⊓ y = (x ⊓ y) \ z
Full source 
/-- See also `inf_sdiff_assoc`. -/
theorem sdiff_inf_right_comm (x y z : α) : x \ zx \ z ⊓ y = (x ⊓ y) \ z := by
  rw [inf_comm x, inf_comm, inf_sdiff_assoc]
Right Commutativity of Meet with Relative Complement: $(x \setminus z) \sqcap y = (x \sqcap y) \setminus z$
Informal description
For any elements $x$, $y$, and $z$ in a generalized Boolean algebra $\alpha$, the meet of the relative complement of $z$ in $x$ with $y$ is equal to the relative complement of $z$ in the meet of $x$ and $y$. That is: $$ (x \setminus z) \sqcap y = (x \sqcap y) \setminus z. $$
inf_sdiff_left_comm theorem
(a b c : α) : a ⊓ (b \ c) = b ⊓ (a \ c)
Full source 
lemma inf_sdiff_left_comm (a b c : α) : a ⊓ (b \ c) = b ⊓ (a \ c) := by
  simp_rw [← inf_sdiff_assoc, inf_comm]
Left Commutativity of Meet with Relative Complement in Generalized Boolean Algebras
Informal description
For any elements $a$, $b$, and $c$ in a generalized Boolean algebra $\alpha$, the meet operation $\sqcap$ commutes with the relative complement operation $\setminus$ in the following way: \[ a \sqcap (b \setminus c) = b \sqcap (a \setminus c). \]
inf_sdiff_distrib_left theorem
(a b c : α) : a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)
Full source 
theorem inf_sdiff_distrib_left (a b c : α) : a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c) := by
  rw [sdiff_inf, sdiff_eq_bot_iff.2 inf_le_left, bot_sup_eq, inf_sdiff_assoc]
Left Distributivity of Meet over Relative Complement: $a \sqcap (b \setminus c) = (a \sqcap b) \setminus (a \sqcap c)$
Informal description
For any elements $a$, $b$, and $c$ in a generalized Boolean algebra $\alpha$, the following equality holds: $$ a \sqcap (b \setminus c) = (a \sqcap b) \setminus (a \sqcap c). $$
inf_sdiff_distrib_right theorem
(a b c : α) : a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c)
Full source 
theorem inf_sdiff_distrib_right (a b c : α) : a \ ba \ b ⊓ c = (a ⊓ c) \ (b ⊓ c) := by
  simp_rw [inf_comm _ c, inf_sdiff_distrib_left]
Right Distributivity of Meet over Relative Complement: $(a \setminus b) \sqcap c = (a \sqcap c) \setminus (b \sqcap c)$
Informal description
For any elements $a$, $b$, and $c$ in a generalized Boolean algebra $\alpha$, the following equality holds: $$ (a \setminus b) \sqcap c = (a \sqcap c) \setminus (b \sqcap c). $$
disjoint_sdiff_comm theorem
: Disjoint (x \ z) y ↔ Disjoint x (y \ z)
Full source 
theorem disjoint_sdiff_comm : DisjointDisjoint (x \ z) y ↔ Disjoint x (y \ z) := by
  simp_rw [disjoint_iff, sdiff_inf_right_comm, inf_sdiff_assoc]
Commutativity of Disjointness with Relative Complement: $(x \setminus z) \perp y \leftrightarrow x \perp (y \setminus z)$
Informal description
For any elements $x$, $y$, and $z$ in a generalized Boolean algebra, the relative complement $x \setminus z$ is disjoint from $y$ if and only if $x$ is disjoint from the relative complement $y \setminus z$. That is: $$ (x \setminus z) \sqcap y = \bot \quad \text{if and only if} \quad x \sqcap (y \setminus z) = \bot. $$
sup_eq_sdiff_sup_sdiff_sup_inf theorem
: x ⊔ y = x \ y ⊔ y \ x ⊔ x ⊓ y
Full source 
theorem sup_eq_sdiff_sup_sdiff_sup_inf : x ⊔ y = x \ yx \ y ⊔ y \ xx \ y ⊔ y \ x ⊔ x ⊓ y :=
  Eq.symm <|
    calc
      x \ yx \ y ⊔ y \ xx \ y ⊔ y \ x ⊔ x ⊓ y = (x \ y ⊔ y \ x ⊔ x) ⊓ (x \ y ⊔ y \ x ⊔ y) := by rw [sup_inf_left]
      _ = (x \ y ⊔ x ⊔ y \ x) ⊓ (x \ y ⊔ (y \ x ⊔ y)) := by ac_rfl
      _ = (x ⊔ y \ x) ⊓ (x \ y ⊔ y) := by rw [sup_sdiff_right, sup_sdiff_right]
      _ = x ⊔ y := by rw [sup_sdiff_self_right, sup_sdiff_self_left, inf_idem]
Decomposition of Join into Relative Differences and Meet in Generalized Boolean Algebras
Informal description
In a generalized Boolean algebra, for any elements $x$ and $y$, the join $x \sqcup y$ can be expressed as the join of their relative differences and their meet, i.e., $$ x \sqcup y = (x \setminus y) \sqcup (y \setminus x) \sqcup (x \sqcap y). $$
sup_lt_of_lt_sdiff_left theorem
(h : y < z \ x) (hxz : x ≤ z) : x ⊔ y < z
Full source 
theorem sup_lt_of_lt_sdiff_left (h : y < z \ x) (hxz : x ≤ z) : x ⊔ y < z := by
  rw [← sup_sdiff_cancel_right hxz]
  refine (sup_le_sup_left h.le _).lt_of_not_le fun h' => h.not_le ?_
  rw [← sdiff_idem]
  exact (sdiff_le_sdiff_of_sup_le_sup_left h').trans sdiff_le
Supremum Strictly Less Than Element When One Component is Less Than Relative Complement
Informal description
For any elements $x, y, z$ in a generalized Boolean algebra, if $y < z \setminus x$ and $x \leq z$, then the supremum $x \sqcup y$ is strictly less than $z$.
sup_lt_of_lt_sdiff_right theorem
(h : x < z \ y) (hyz : y ≤ z) : x ⊔ y < z
Full source 
theorem sup_lt_of_lt_sdiff_right (h : x < z \ y) (hyz : y ≤ z) : x ⊔ y < z := by
  rw [← sdiff_sup_cancel hyz]
  refine (sup_le_sup_right h.le _).lt_of_not_le fun h' => h.not_le ?_
  rw [← sdiff_idem]
  exact (sdiff_le_sdiff_of_sup_le_sup_right h').trans sdiff_le
Join Strictly Less Than Upper Bound via Right Difference: $x < z \setminus y \land y \leq z \Rightarrow x \sqcup y < z$
Informal description
Let $\alpha$ be a generalized Boolean algebra. For any elements $x, y, z \in \alpha$, if $x$ is strictly less than the relative complement $z \setminus y$ and $y$ is less than or equal to $z$, then the join $x \sqcup y$ is strictly less than $z$.
Prod.instGeneralizedBooleanAlgebra instance
[GeneralizedBooleanAlgebra β] : GeneralizedBooleanAlgebra (α × β)
Full source 
instance Prod.instGeneralizedBooleanAlgebra [GeneralizedBooleanAlgebra β] :
    GeneralizedBooleanAlgebra (α × β) where
  sup_inf_sdiff _ _ := Prod.ext (sup_inf_sdiff _ _) (sup_inf_sdiff _ _)
  inf_inf_sdiff _ _ := Prod.ext (inf_inf_sdiff _ _) (inf_inf_sdiff _ _)
Componentwise Generalized Boolean Algebra Structure on Products
Informal description
For any generalized Boolean algebra $\beta$, the product type $\alpha \times \beta$ is also a generalized Boolean algebra, where the lattice operations, bottom element, and relative complement operation are defined componentwise. Specifically: - The join $(a_1, b_1) \sqcup (a_2, b_2) = (a_1 \sqcup a_2, b_1 \sqcup b_2)$ - The meet $(a_1, b_1) \sqcap (a_2, b_2) = (a_1 \sqcap a_2, b_1 \sqcap b_2)$ - The bottom element $\bot = (\bot, \bot)$ - The relative complement $(a_1, b_1) \setminus (a_2, b_2) = (a_1 \setminus a_2, b_1 \setminus b_2)$
Pi.instGeneralizedBooleanAlgebra instance
{ι : Type*} {α : ι → Type*} [∀ i, GeneralizedBooleanAlgebra (α i)] : GeneralizedBooleanAlgebra (∀ i, α i)
Full source 
instance Pi.instGeneralizedBooleanAlgebra {ι : Type*} {α : ι → Type*}
    [∀ i, GeneralizedBooleanAlgebra (α i)] : GeneralizedBooleanAlgebra (∀ i, α i) where
  sup_inf_sdiff := fun f g => funext fun a => sup_inf_sdiff (f a) (g a)
  inf_inf_sdiff := fun f g => funext fun a => inf_inf_sdiff (f a) (g a)
Pointwise Generalized Boolean Algebra Structure on Product Types
Informal description
For any family of types $(\alpha_i)_{i \in \iota}$ where each $\alpha_i$ is a generalized Boolean algebra, the product type $\forall i, \alpha_i$ is also a generalized Boolean algebra with pointwise operations. Specifically: 1. The lattice operations $\sqcap$ and $\sqcup$ are defined pointwise as $(f \sqcap g)(i) = f(i) \sqcap g(i)$ and $(f \sqcup g)(i) = f(i) \sqcup g(i)$. 2. The relative complement operation $\setminus$ is defined pointwise as $(f \setminus g)(i) = f(i) \setminus g(i)$. 3. The bottom element $\bot$ is defined pointwise as $\bot(i) = \bot_{\alpha_i}$.
BooleanAlgebra structure
(α : Type u) extends DistribLattice α, HasCompl α, SDiff α, HImp α, Top α, Bot α
Full source 
/-- 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.
-/
class BooleanAlgebra (α : Type u) extends
    DistribLattice α, HasCompl α, SDiff α, HImp α, Top α, Bot α where
  /-- The infimum of `x` and `xᶜ` is at most `⊥` -/
  inf_compl_le_bot : ∀ x : α, x ⊓ xᶜ ≤ ⊥
  /-- The supremum of `x` and `xᶜ` is at least `⊤` -/
  top_le_sup_compl : ∀ x : α, ⊤ ≤ x ⊔ xᶜ
  /-- `⊤` is the greatest element -/
  le_top : ∀ a : α, a ≤ ⊤
  /-- `⊥` is the least element -/
  bot_le : ∀ a : α, ⊥ ≤ a
  /-- `x \ y` is equal to `x ⊓ yᶜ` -/
  sdiff := fun x y => x ⊓ yᶜ
  /-- `x ⇨ y` is equal to `y ⊔ xᶜ` -/
  himp := fun x y => y ⊔ xᶜ
  /-- `x \ y` is equal to `x ⊓ yᶜ` -/
  sdiff_eq : ∀ x y : α, x \ y = x ⊓ yᶜ := by aesop
  /-- `x ⇨ y` is equal to `y ⊔ xᶜ` -/
  himp_eq : ∀ x y : α, x ⇨ y = y ⊔ xᶜ := by aesop
Boolean algebra
Informal description
A Boolean algebra is a bounded distributive lattice $(α, ⊓, ⊔, ⊥, ⊤)$ equipped with a complement operator $(\cdot)^\complement$, a set difference operation $\setminus$, and a Heyting implication $\Rightarrow$ satisfying: 1. $x ⊓ x^\complement = ⊥$ and $x ⊔ x^\complement = ⊤$ for all $x ∈ α$, 2. $x \setminus y = x ⊓ y^\complement$ for all $x, y ∈ α$, 3. $x \Rightarrow y = y ⊔ x^\complement$ for all $x, y ∈ α$. This structure generalizes classical propositional logic and the lattice of subsets of a set.
BooleanAlgebra.toBoundedOrder instance
[h : BooleanAlgebra α] : BoundedOrder α
Full source 
instance (priority := 100) BooleanAlgebra.toBoundedOrder [h : BooleanAlgebra α] : BoundedOrder α :=
  { h with }
Boolean Algebras are Bounded Orders
Informal description
Every Boolean algebra is a bounded order. That is, for any Boolean algebra $\alpha$, there exist both a greatest element $\top$ and a least element $\bot$ in $\alpha$.
GeneralizedBooleanAlgebra.toBooleanAlgebra abbrev
[GeneralizedBooleanAlgebra α] [OrderTop α] : BooleanAlgebra α
Full source 
/-- A bounded generalized boolean algebra is a boolean algebra. -/
abbrev GeneralizedBooleanAlgebra.toBooleanAlgebra [GeneralizedBooleanAlgebra α] [OrderTop α] :
    BooleanAlgebra α where
  __ := ‹GeneralizedBooleanAlgebra α›
  __ := GeneralizedBooleanAlgebra.toOrderBot
  __ := ‹OrderTop α›
  compl a := ⊤⊤ \ a
  inf_compl_le_bot _ := disjoint_sdiff_self_right.le_bot
  top_le_sup_compl _ := le_sup_sdiff
  sdiff_eq a b := by
    change _ = a ⊓ (⊤ \ b)
    rw [← inf_sdiff_assoc, inf_top_eq]
Generalized Boolean Algebra with Top is Boolean Algebra
Informal description
Every generalized Boolean algebra $\alpha$ with a top element $\top$ forms a Boolean algebra.
inf_compl_eq_bot' theorem
: x ⊓ xᶜ = ⊥
Full source 
theorem inf_compl_eq_bot' : x ⊓ xᶜ = ⊥ :=
  bot_unique <| BooleanAlgebra.inf_compl_le_bot x
Complement Meet Identity: $x ⊓ x^\complement = \bot$
Informal description
For any element $x$ in a Boolean algebra, the meet of $x$ and its complement $x^\complement$ equals the bottom element $\bot$, i.e., $x ⊓ x^\complement = \bot$.
sup_compl_eq_top theorem
: x ⊔ xᶜ = ⊤
Full source 
@[simp]
theorem sup_compl_eq_top : x ⊔ xᶜ = ⊤ :=
  top_unique <| BooleanAlgebra.top_le_sup_compl x
Complement Supremum Identity: $x \sqcup x^\complement = \top$
Informal description
For any element $x$ in a Boolean algebra, the supremum of $x$ and its complement $x^\complement$ equals the top element $\top$, i.e., $x \sqcup x^\complement = \top$.
compl_sup_eq_top theorem
: xᶜ ⊔ x = ⊤
Full source 
@[simp]
theorem compl_sup_eq_top : xᶜxᶜ ⊔ x = ⊤ := by rw [sup_comm, sup_compl_eq_top]
Complement Supremum Identity: $x^\complement \sqcup x = \top$
Informal description
For any element $x$ in a Boolean algebra, the supremum of the complement $x^\complement$ and $x$ equals the top element $\top$, i.e., $x^\complement \sqcup x = \top$.
isCompl_compl theorem
: IsCompl x xᶜ
Full source 
theorem isCompl_compl : IsCompl x xᶜ :=
  IsCompl.of_eq inf_compl_eq_bot' sup_compl_eq_top
Complementary Pair: $x$ and $x^\complement$
Informal description
For any element $x$ in a Boolean algebra, $x$ and its complement $x^\complement$ are complementary elements, meaning they satisfy $x \sqcap x^\complement = \bot$ and $x \sqcup x^\complement = \top$.
sdiff_eq theorem
: x \ y = x ⊓ yᶜ
Full source 
theorem sdiff_eq : x \ y = x ⊓ yᶜ :=
  BooleanAlgebra.sdiff_eq x y
Set Difference Equals Meet with Complement: $x \setminus y = x \sqcap y^\complement$
Informal description
In a Boolean algebra, the set difference operation $\setminus$ satisfies $x \setminus y = x \sqcap y^\complement$ for all elements $x$ and $y$.
himp_eq theorem
: x ⇨ y = y ⊔ xᶜ
Full source 
theorem himp_eq : x ⇨ y = y ⊔ xᶜ :=
  BooleanAlgebra.himp_eq x y
Heyting Implication as Supremum with Complement: $x \Rightarrow y = y \sqcup x^\complement$
Informal description
In a Boolean algebra, the Heyting implication operation $\Rightarrow$ satisfies $x \Rightarrow y = y \sqcup x^\complement$ for all elements $x$ and $y$.
BooleanAlgebra.toComplementedLattice instance
: ComplementedLattice α
Full source 
instance (priority := 100) BooleanAlgebra.toComplementedLattice : ComplementedLattice α :=
  ⟨fun x => ⟨xᶜ, isCompl_compl⟩⟩
Boolean Algebras are Complemented Lattices
Informal description
Every Boolean algebra is a complemented lattice. That is, for any Boolean algebra $\alpha$, every element $x \in \alpha$ has a complement $x^\complement$ satisfying $x \sqcap x^\complement = \bot$ and $x \sqcup x^\complement = \top$.
BooleanAlgebra.toGeneralizedBooleanAlgebra instance
: GeneralizedBooleanAlgebra α
Full source 
instance (priority := 100) BooleanAlgebra.toGeneralizedBooleanAlgebra :
    GeneralizedBooleanAlgebra α where
  __ := ‹BooleanAlgebra α›
  sup_inf_sdiff a b := by rw [sdiff_eq, ← inf_sup_left, sup_compl_eq_top, inf_top_eq]
  inf_inf_sdiff a b := by
    rw [sdiff_eq, ← inf_inf_distrib_left, inf_compl_eq_bot', inf_bot_eq]
Boolean Algebras as Generalized Boolean Algebras
Informal description
Every Boolean algebra is a generalized Boolean algebra.
BooleanAlgebra.toBiheytingAlgebra instance
: BiheytingAlgebra α
Full source 
instance (priority := 100) BooleanAlgebra.toBiheytingAlgebra : BiheytingAlgebra α where
  __ := ‹BooleanAlgebra α›
  __ := GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra
  hnot := compl
  le_himp_iff a b c := by rw [himp_eq, isCompl_compl.le_sup_right_iff_inf_left_le]
  himp_bot _ := _root_.himp_eq.trans (bot_sup_eq _)
  top_sdiff a := by rw [sdiff_eq, top_inf_eq]
Boolean Algebras are Bi-Heyting Algebras
Informal description
Every Boolean algebra is a bi-Heyting algebra. This means that in addition to the usual Boolean algebra structure, it also carries both Heyting and co-Heyting algebra structures, with operations including implication $\Rightarrow$, co-implication $\setminus$, and negation $\neg$.
hnot_eq_compl theorem
: ￢x = xᶜ
Full source 
@[simp]
theorem hnot_eq_compl : ￢x = xᶜ :=
  rfl
Heyting Negation Equals Complement in Boolean Algebras
Informal description
In a Boolean algebra, the Heyting negation $\neg x$ is equal to the complement $x^\complement$ for any element $x$.
top_sdiff theorem
: ⊤ \ x = xᶜ
Full source 
theorem top_sdiff : ⊤⊤ \ x = xᶜ :=
  top_sdiff' x
Top difference equals complement in Boolean algebra
Informal description
In a Boolean algebra $\alpha$, for any element $x \in \alpha$, the difference between the top element $\top$ and $x$ equals the complement of $x$, i.e., $\top \setminus x = x^\complement$.
compl_compl theorem
(x : α) : xᶜᶜ = x
Full source 
@[simp]
theorem compl_compl (x : α) : xᶜxᶜᶜ = x :=
  (@isCompl_compl _ x _).symm.compl_eq
Double Complement Law: $(x^\complement)^\complement = x$
Informal description
For any element $x$ in a Boolean algebra, the complement of the complement of $x$ is equal to $x$ itself, i.e., $(x^\complement)^\complement = x$.
compl_comp_compl theorem
: compl ∘ compl = @id α
Full source 
theorem compl_comp_compl : complcompl ∘ compl = @id α :=
  funext compl_compl
Double Complement Composition: $(\cdot)^\complement \circ (\cdot)^\complement = \text{id}_\alpha$
Informal description
The composition of the complement operator with itself is equal to the identity function on $\alpha$, i.e., $(\cdot)^\complement \circ (\cdot)^\complement = \text{id}_\alpha$.
compl_involutive theorem
: Function.Involutive (compl : α → α)
Full source 
@[simp]
theorem compl_involutive : Function.Involutive (compl : α → α) :=
  compl_compl
Involutive Property of Boolean Complement: $(x^\complement)^\complement = x$
Informal description
The complement operation $(\cdot)^\complement$ in a Boolean algebra is involutive, meaning that for any element $x$ in the Boolean algebra, applying the complement operation twice returns the original element: $(x^\complement)^\complement = x$.
compl_bijective theorem
: Function.Bijective (compl : α → α)
Full source 
theorem compl_bijective : Function.Bijective (compl : α → α) :=
  compl_involutive.bijective
Bijectivity of Boolean Complement Operation
Informal description
The complement operation $(\cdot)^\complement$ in a Boolean algebra is bijective, meaning it is both injective and surjective. That is: 1. For any $x, y \in \alpha$, if $x^\complement = y^\complement$ then $x = y$ (injective). 2. For every $y \in \alpha$, there exists an $x \in \alpha$ such that $x^\complement = y$ (surjective).
compl_surjective theorem
: Function.Surjective (compl : α → α)
Full source 
theorem compl_surjective : Function.Surjective (compl : α → α) :=
  compl_involutive.surjective
Surjectivity of Boolean Complement Operation
Informal description
The complement operation $(\cdot)^\complement$ in a Boolean algebra is surjective, meaning that for every element $y$ in the Boolean algebra, there exists an element $x$ such that $x^\complement = y$.
compl_injective theorem
: Function.Injective (compl : α → α)
Full source 
theorem compl_injective : Function.Injective (compl : α → α) :=
  compl_involutive.injective
Injectivity of Boolean Complement: $x^\complement = y^\complement \Rightarrow x = y$
Informal description
The complement operation $(\cdot)^\complement$ in a Boolean algebra is injective, meaning that for any elements $x$ and $y$ in the Boolean algebra, if $x^\complement = y^\complement$ then $x = y$.
compl_inj_iff theorem
: xᶜ = yᶜ ↔ x = y
Full source 
@[simp]
theorem compl_inj_iff : xᶜxᶜ = yᶜ ↔ x = y :=
  compl_injective.eq_iff
Complement Equality Criterion: $x^\complement = y^\complement \leftrightarrow x = y$
Informal description
For any elements $x$ and $y$ in a Boolean algebra, the complements $x^\complement$ and $y^\complement$ are equal if and only if $x = y$.
IsCompl.compl_eq_iff theorem
(h : IsCompl x y) : zᶜ = y ↔ z = x
Full source 
theorem IsCompl.compl_eq_iff (h : IsCompl x y) : zᶜzᶜ = y ↔ z = x :=
  h.compl_eq ▸ compl_inj_iff
Complement Characterization for Complementary Elements: $z^\complement = y \leftrightarrow z = x$ when $x$ and $y$ are complements
Informal description
Let $x$ and $y$ be complementary elements in a Boolean algebra (i.e., $x \sqcap y = \bot$ and $x \sqcup y = \top$). Then for any element $z$ in the algebra, the complement $z^\complement$ equals $y$ if and only if $z = x$.
compl_eq_top theorem
: xᶜ = ⊤ ↔ x = ⊥
Full source 
@[simp]
theorem compl_eq_top : xᶜxᶜ = ⊤ ↔ x = ⊥ :=
  isCompl_bot_top.compl_eq_iff
Complement Equals Top iff Element is Bottom
Informal description
For any element $x$ in a Boolean algebra, the complement of $x$ equals the top element $\top$ if and only if $x$ is the bottom element $\bot$, i.e., $$x^\complement = \top \leftrightarrow x = \bot.$$
compl_eq_bot theorem
: xᶜ = ⊥ ↔ x = ⊤
Full source 
@[simp]
theorem compl_eq_bot : xᶜxᶜ = ⊥ ↔ x = ⊤ :=
  isCompl_top_bot.compl_eq_iff
Complement Characterization: $x^\complement = \bot \leftrightarrow x = \top$
Informal description
In a Boolean algebra, the complement of an element $x$ equals the bottom element $\bot$ if and only if $x$ is the top element $\top$, i.e., $x^\complement = \bot \leftrightarrow x = \top$.
compl_inf theorem
: (x ⊓ y)ᶜ = xᶜ ⊔ yᶜ
Full source 
@[simp]
theorem compl_inf : (x ⊓ y)ᶜ = xᶜxᶜ ⊔ yᶜ :=
  hnot_inf_distrib _ _
De Morgan's Law for Complements in Boolean Algebras: $(x \sqcap y)^\complement = x^\complement \sqcup y^\complement$
Informal description
In a Boolean algebra $\alpha$, for any elements $x, y \in \alpha$, the complement of their meet equals the join of their complements, i.e., $$(x \sqcap y)^\complement = x^\complement \sqcup y^\complement.$$
compl_le_compl_iff_le theorem
: yᶜ ≤ xᶜ ↔ x ≤ y
Full source 
@[simp]
theorem compl_le_compl_iff_le : yᶜyᶜ ≤ xᶜ ↔ x ≤ y :=
  ⟨fun h => by have h := compl_le_compl h; simpa using h, compl_le_compl⟩
Order Reversal of Complements: $y^\complement \leq x^\complement \leftrightarrow x \leq y$
Informal description
For any elements $x$ and $y$ in a Boolean algebra, the complement of $y$ is less than or equal to the complement of $x$ if and only if $x$ is less than or equal to $y$. In symbols: $$ y^\complement \leq x^\complement \leftrightarrow x \leq y $$
compl_lt_compl_iff_lt theorem
: yᶜ < xᶜ ↔ x < y
Full source 
@[simp] lemma compl_lt_compl_iff_lt : yᶜyᶜ < xᶜ ↔ x < y :=
  lt_iff_lt_of_le_iff_le' compl_le_compl_iff_le compl_le_compl_iff_le
Strict Order Reversal of Complements: $y^\complement < x^\complement \leftrightarrow x < y$
Informal description
For any elements $x$ and $y$ in a Boolean algebra, the complement of $y$ is strictly less than the complement of $x$ if and only if $x$ is strictly less than $y$. In symbols: $$ y^\complement < x^\complement \leftrightarrow x < y $$
compl_le_of_compl_le theorem
(h : yᶜ ≤ x) : xᶜ ≤ y
Full source 
theorem compl_le_of_compl_le (h : yᶜ ≤ x) : xᶜ ≤ y := by
  simpa only [compl_compl] using compl_le_compl h
Complement Order Reversal: $y^\complement \leq x \implies x^\complement \leq y$
Informal description
In a Boolean algebra, if the complement of an element $y$ is less than or equal to an element $x$, then the complement of $x$ is less than or equal to $y$, i.e., $y^\complement \leq x$ implies $x^\complement \leq y$.
compl_le_iff_compl_le theorem
: xᶜ ≤ y ↔ yᶜ ≤ x
Full source 
theorem compl_le_iff_compl_le : xᶜxᶜ ≤ y ↔ yᶜ ≤ x :=
  ⟨compl_le_of_compl_le, compl_le_of_compl_le⟩
Complement Order Reversal Equivalence: $x^\complement \leq y \leftrightarrow y^\complement \leq x$
Informal description
For any elements $x$ and $y$ in a Boolean algebra, the complement of $x$ is less than or equal to $y$ if and only if the complement of $y$ is less than or equal to $x$, i.e., $x^\complement \leq y \leftrightarrow y^\complement \leq x$.
compl_le_self theorem
: xᶜ ≤ x ↔ x = ⊤
Full source 
@[simp] theorem compl_le_self : xᶜxᶜ ≤ x ↔ x = ⊤ := by simpa using le_compl_self (a := xᶜ)
Characterization of Top Element via Complement Inequality: $x^\complement \leq x \leftrightarrow x = \top$
Informal description
For any element $x$ in a Boolean algebra, the complement of $x$ is less than or equal to $x$ if and only if $x$ is equal to the top element $\top$, i.e., $x^\complement \leq x \leftrightarrow x = \top$.
compl_lt_self theorem
[Nontrivial α] : xᶜ < x ↔ x = ⊤
Full source 
@[simp] theorem compl_lt_self [Nontrivial α] : xᶜxᶜ < x ↔ x = ⊤ := by
  simpa using lt_compl_self (a := xᶜ)
Characterization of Top Element via Complement in Nontrivial Boolean Algebra
Informal description
In a nontrivial Boolean algebra $\alpha$, for any element $x \in \alpha$, the strict inequality $x^\complement < x$ holds if and only if $x$ is the top element $\top$.
sdiff_compl theorem
: x \ yᶜ = x ⊓ y
Full source 
@[simp]
theorem sdiff_compl : x \ yᶜ = x ⊓ y := by rw [sdiff_eq, compl_compl]
Set Difference with Complement Equals Meet: $x \setminus y^\complement = x \sqcap y$
Informal description
For any elements $x$ and $y$ in a Boolean algebra, the set difference $x \setminus y^\complement$ equals the meet of $x$ and $y$, i.e., $x \setminus y^\complement = x \sqcap y$.
OrderDual.instBooleanAlgebra instance
: BooleanAlgebra αᵒᵈ
Full source 
instance OrderDual.instBooleanAlgebra : BooleanAlgebra αᵒᵈ where
  __ := instDistribLattice α
  __ := instHeytingAlgebra
  sdiff_eq _ _ := @himp_eq α _ _ _
  himp_eq _ _ := @sdiff_eq α _ _ _
  inf_compl_le_bot a := (@codisjoint_hnot_right _ _ (ofDual a)).top_le
  top_le_sup_compl a := (@disjoint_compl_right _ _ (ofDual a)).le_bot
Order Dual of a Boolean Algebra is a Boolean Algebra
Informal description
For any Boolean algebra $\alpha$, the order dual $\alpha^{\text{op}}$ is also a Boolean algebra, with the operations defined dually. Specifically: - The complement operation remains the same. - The meet $\sqcap$ and join $\sqcup$ operations are swapped. - The top element $\top$ and bottom element $\bot$ are swapped. - The set difference $\setminus$ and Heyting implication $\Rightarrow$ operations are swapped.
sup_inf_inf_compl theorem
: x ⊓ y ⊔ x ⊓ yᶜ = x
Full source 
@[simp]
theorem sup_inf_inf_compl : x ⊓ yx ⊓ y ⊔ x ⊓ yᶜ = x := by rw [← sdiff_eq, sup_inf_sdiff _ _]
Join of Meet and Complemented Meet Equals Original Element
Informal description
For any elements $x$ and $y$ in a Boolean algebra, the join of $x \sqcap y$ and $x \sqcap y^\complement$ equals $x$, i.e., $(x \sqcap y) \sqcup (x \sqcap y^\complement) = x$.
compl_sdiff theorem
: (x \ y)ᶜ = x ⇨ y
Full source 
theorem compl_sdiff : (x \ y)ᶜ = x ⇨ y := by
  rw [sdiff_eq, himp_eq, compl_inf, compl_compl, sup_comm]
Complement of Set Difference Equals Heyting Implication: $(x \setminus y)^\complement = x \Rightarrow y$
Informal description
In a Boolean algebra, the complement of the set difference $x \setminus y$ is equal to the Heyting implication $x \Rightarrow y$, i.e., $(x \setminus y)^\complement = x \Rightarrow y$.
compl_himp theorem
: (x ⇨ y)ᶜ = x \ y
Full source 
@[simp]
theorem compl_himp : (x ⇨ y)ᶜ = x \ y :=
  @compl_sdiff αᵒᵈ _ _ _
Complement of Heyting Implication Equals Set Difference: $(x \Rightarrow y)^\complement = x \setminus y$
Informal description
In a Boolean algebra, the complement of the Heyting implication $x \Rightarrow y$ is equal to the set difference $x \setminus y$, i.e., $(x \Rightarrow y)^\complement = x \setminus y$.
compl_sdiff_compl theorem
: xᶜ \ yᶜ = y \ x
Full source 
theorem compl_sdiff_compl : xᶜxᶜ \ yᶜ = y \ x := by rw [sdiff_compl, sdiff_eq, inf_comm]
Complement Set Difference Identity: $x^\complement \setminus y^\complement = y \setminus x$
Informal description
For any elements $x$ and $y$ in a Boolean algebra, the set difference of the complements satisfies $x^\complement \setminus y^\complement = y \setminus x$.
compl_himp_compl theorem
: xᶜ ⇨ yᶜ = y ⇨ x
Full source 
@[simp]
theorem compl_himp_compl : xᶜxᶜ ⇨ yᶜ = y ⇨ x :=
  @compl_sdiff_compl αᵒᵈ _ _ _
Heyting Implication Identity for Complements: $x^\complement \Rightarrow y^\complement = y \Rightarrow x$
Informal description
For any elements $x$ and $y$ in a Boolean algebra, the Heyting implication of their complements satisfies $x^\complement \Rightarrow y^\complement = y \Rightarrow x$.
disjoint_compl_left_iff theorem
: Disjoint xᶜ y ↔ y ≤ x
Full source 
theorem disjoint_compl_left_iff : DisjointDisjoint xᶜ y ↔ y ≤ x := by
  rw [← le_compl_iff_disjoint_left, compl_compl]
Disjointness of Complement Characterizes Order: $\text{Disjoint}(x^\complement, y) \leftrightarrow y \leq x$
Informal description
For any elements $x$ and $y$ in a Boolean algebra, the complement of $x$ is disjoint from $y$ if and only if $y$ is less than or equal to $x$. In symbols: \[ \text{Disjoint}(x^\complement, y) \leftrightarrow y \leq x \]
codisjoint_himp_self_left theorem
: Codisjoint (x ⇨ y) x
Full source 
theorem codisjoint_himp_self_left : Codisjoint (x ⇨ y) x :=
  @disjoint_sdiff_self_left αᵒᵈ _ _ _
Codisjointness of Heyting Implication: $(x \Rightarrow y) \sqcup x = \top$
Informal description
For any elements $x$ and $y$ in a Boolean algebra, the Heyting implication $(x \Rightarrow y)$ and $x$ are codisjoint, i.e., $(x \Rightarrow y) \sqcup x = \top$.
codisjoint_himp_self_right theorem
: Codisjoint x (x ⇨ y)
Full source 
theorem codisjoint_himp_self_right : Codisjoint x (x ⇨ y) :=
  @disjoint_sdiff_self_right αᵒᵈ _ _ _
Codisjointness of Element with Its Heyting Implication: $x \sqcup (x \Rightarrow y) = \top$
Informal description
For any elements $x$ and $y$ in a Boolean algebra, the element $x$ and its Heyting implication $x \Rightarrow y$ are codisjoint, i.e., $x \sqcup (x \Rightarrow y) = \top$.
himp_le theorem
: x ⇨ y ≤ z ↔ y ≤ z ∧ Codisjoint x z
Full source 
theorem himp_le : x ⇨ yx ⇨ y ≤ z ↔ y ≤ z ∧ Codisjoint x z :=
  (@le_sdiff αᵒᵈ _ _ _ _).trans <| and_congr_right' <| @codisjoint_comm _ (_) _ _ _
Characterization of Heyting Implication Order via Codisjointness: $x \Rightarrow y \leq z \leftrightarrow (y \leq z \land x \sqcup z = \top)$
Informal description
For any elements $x$, $y$, and $z$ in a Boolean algebra, the Heyting implication $x \Rightarrow y$ is less than or equal to $z$ if and only if $y$ is less than or equal to $z$ and $x$ and $z$ are codisjoint (i.e., $x \sqcup z = \top$).
himp_eq_left theorem
: x ⇨ y = x ↔ x = ⊤ ∧ y = ⊤
Full source 
@[simp] lemma himp_eq_left : x ⇨ yx ⇨ y = x ↔ x = ⊤ ∧ y = ⊤ := by
  rw [codisjoint_himp_self_left.eq_iff]; aesop
Heyting Implication Equals Left Operand iff Both Are Top
Informal description
For any elements $x$ and $y$ in a Boolean algebra, the Heyting implication $x \Rightarrow y$ is equal to $x$ if and only if $x$ is the top element $\top$ and $y$ is the top element $\top$, i.e., $x \Rightarrow y = x \leftrightarrow (x = \top \land y = \top)$.
himp_ne_right theorem
: x ⇨ y ≠ x ↔ x ≠ ⊤ ∨ y ≠ ⊤
Full source 
lemma himp_ne_right : x ⇨ yx ⇨ y ≠ xx ⇨ y ≠ x ↔ x ≠ ⊤ ∨ y ≠ ⊤ := himp_eq_left.not.trans not_and_or
Heyting Implication Inequality: $x \Rightarrow y \neq x \leftrightarrow x \neq \top \lor y \neq \top$
Informal description
For any elements $x$ and $y$ in a Boolean algebra, the Heyting implication $x \Rightarrow y$ is not equal to $x$ if and only if $x$ is not the top element $\top$ or $y$ is not the top element $\top$, i.e., $x \Rightarrow y \neq x \leftrightarrow (x \neq \top \lor y \neq \top)$.
codisjoint_iff_compl_le_left theorem
: Codisjoint x y ↔ yᶜ ≤ x
Full source 
lemma codisjoint_iff_compl_le_left : CodisjointCodisjoint x y ↔ yᶜ ≤ x :=
  hnot_le_iff_codisjoint_left.symm
Codisjointness via Complement Inequality: $x \sqcup y = \top \leftrightarrow y^\complement \leq x$
Informal description
For elements $x$ and $y$ in a Boolean algebra, $x$ and $y$ are codisjoint (i.e., $x \sqcup y = \top$) if and only if the complement of $y$ is less than or equal to $x$ (i.e., $y^\complement \leq x$).
Prop.instBooleanAlgebra instance
: BooleanAlgebra Prop
Full source 
instance Prop.instBooleanAlgebra : BooleanAlgebra Prop where
  __ := Prop.instHeytingAlgebra
  __ := GeneralizedHeytingAlgebra.toDistribLattice
  compl := Not
  himp_eq _ _ := propext imp_iff_or_not
  inf_compl_le_bot _ H := H.2 H.1
  top_le_sup_compl p _ := Classical.em p
Boolean Algebra Structure on Propositions
Informal description
The set of propositions forms a Boolean algebra, where: - The meet operation $\sqcap$ corresponds to logical conjunction (and) - The join operation $\sqcup$ corresponds to logical disjunction (or) - The complement operation $(\cdot)^\complement$ corresponds to logical negation - The top element $\top$ corresponds to true - The bottom element $\bot$ corresponds to false This structure models classical propositional logic.
Prod.instBooleanAlgebra instance
[BooleanAlgebra α] [BooleanAlgebra β] : BooleanAlgebra (α × β)
Full source 
instance Prod.instBooleanAlgebra [BooleanAlgebra α] [BooleanAlgebra β] :
    BooleanAlgebra (α × β) where
  __ := instDistribLattice α β
  __ := instHeytingAlgebra
  himp_eq x y := by ext <;> simp [himp_eq]
  sdiff_eq x y := by ext <;> simp [sdiff_eq]
  inf_compl_le_bot x := by constructor <;> simp
  top_le_sup_compl x := by constructor <;> simp
Componentwise Boolean Algebra Structure on Products
Informal description
For any two Boolean algebras $\alpha$ and $\beta$, the product $\alpha \times \beta$ is also a Boolean algebra, with all operations defined componentwise. Specifically: - The meet operation is $(a_1, b_1) \sqcap (a_2, b_2) = (a_1 \sqcap a_2, b_1 \sqcap b_2)$, - The join operation is $(a_1, b_1) \sqcup (a_2, b_2) = (a_1 \sqcup a_2, b_1 \sqcup b_2)$, - The complement operation is $(a, b)^\complement = (a^\complement, b^\complement)$, - The top element is $(\top, \top)$, - The bottom element is $(\bot, \bot)$.
Pi.instBooleanAlgebra instance
{ι : Type u} {α : ι → Type v} [∀ i, BooleanAlgebra (α i)] : BooleanAlgebra (∀ i, α i)
Full source 
instance Pi.instBooleanAlgebra {ι : Type u} {α : ι → Type v} [∀ i, BooleanAlgebra (α i)] :
    BooleanAlgebra (∀ i, α i) where
  __ := instDistribLattice
  __ := instHeytingAlgebra
  sdiff_eq _ _ := funext fun _ => sdiff_eq
  himp_eq _ _ := funext fun _ => himp_eq
  inf_compl_le_bot _ _ := BooleanAlgebra.inf_compl_le_bot _
  top_le_sup_compl _ _ := BooleanAlgebra.top_le_sup_compl _
Pointwise Boolean Algebra Structure on Product Types
Informal description
For any family of Boolean algebras $(α_i)_{i \in \iota}$, the product type $\prod_{i \in \iota} α_i$ is also a Boolean algebra, with all operations (meet $\sqcap$, join $\sqcup$, complement $(\cdot)^\complement$, set difference $\setminus$, Heyting implication $\Rightarrow$, top $\top$, and bottom $\bot$) defined pointwise. Specifically: 1. $(f \sqcap g)(i) = f(i) \sqcap g(i)$, 2. $(f \sqcup g)(i) = f(i) \sqcup g(i)$, 3. $f^\complement(i) = (f(i))^\complement$, 4. $(f \setminus g)(i) = f(i) \setminus g(i)$, 5. $(f \Rightarrow g)(i) = f(i) \Rightarrow g(i)$, 6. $\top(i) = \top$, 7. $\bot(i) = \bot$, for all $i \in \iota$ and $f, g \in \prod_{i \in \iota} α_i$.
Bool.instBooleanAlgebra instance
: BooleanAlgebra Bool
Full source 
instance Bool.instBooleanAlgebra : BooleanAlgebra Bool where
  __ := instBoundedOrder
  compl := not
  inf_compl_le_bot a := a.and_not_self.le
  top_le_sup_compl a := a.or_not_self.ge
Boolean Algebra Structure on Boolean Values
Informal description
The Boolean type `Bool` is a Boolean algebra, where the operations are defined as follows: - The meet operation $\sqcap$ is logical AND, - The join operation $\sqcup$ is logical OR, - The complement operation $(\cdot)^\complement$ is logical NOT, - The top element $\top$ is `true`, - The bottom element $\bot$ is `false`.
Bool.sup_eq_bor theorem
: (· ⊔ ·) = or
Full source 
theorem Bool.sup_eq_bor : (· ⊔ ·) = or := by dsimp
Supremum Equals Logical OR in Boolean Algebra
Informal description
The supremum operation $\sqcup$ on the Boolean type `Bool` coincides with the logical OR operation `or`.
Bool.inf_eq_band theorem
: (· ⊓ ·) = and
Full source 
theorem Bool.inf_eq_band : (· ⊓ ·) = and := by dsimp
Infimum Equals Logical AND in Boolean Algebra
Informal description
The infimum operation on the Boolean type `Bool` coincides with the logical AND operation, i.e., for any two Boolean values `x` and `y`, we have $x \sqcap y = x \land y$.
Bool.compl_eq_bnot theorem
: HasCompl.compl = not
Full source 
@[simp]
theorem Bool.compl_eq_bnot : HasCompl.compl = not :=
  rfl
Boolean Complement Equals Logical NOT
Informal description
The complement operation in the Boolean algebra structure on the Boolean type `Bool` coincides with the logical NOT operation, i.e., for any Boolean value `x`, we have $x^\complement = \lnot x$.
Function.Injective.generalizedBooleanAlgebra abbrev
[Max α] [Min α] [Bot α] [SDiff α] [GeneralizedBooleanAlgebra β] (f : α → β) (hf : 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) : GeneralizedBooleanAlgebra α
Full source 
/-- Pullback a `GeneralizedBooleanAlgebra` along an injection. -/
protected abbrev Function.Injective.generalizedBooleanAlgebra [Max α] [Min α] [Bot α] [SDiff α]
    [GeneralizedBooleanAlgebra β] (f : α → β) (hf : 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) :
    GeneralizedBooleanAlgebra α where
  __ := hf.generalizedCoheytingAlgebra f map_sup map_inf map_bot map_sdiff
  __ := hf.distribLattice f map_sup map_inf
  sup_inf_sdiff a b := hf <| by rw [map_sup, map_sdiff, map_inf, sup_inf_sdiff]
  inf_inf_sdiff a b := hf <| by rw [map_inf, map_sdiff, map_inf, inf_inf_sdiff, map_bot]
Pullback of Generalized Boolean Algebra Structure Along an Injective Function
Informal description
Let $\alpha$ and $\beta$ be types equipped with lattice structures, where $\beta$ is a generalized Boolean algebra. Given an injective function $f \colon \alpha \to \beta$ that preserves: - Suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$ for all $a, b \in \alpha$, - Infima: $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$, - Bottom element: $f(\bot) = \bot$, - Relative complement: $f(a \setminus b) = f(a) \setminus f(b)$ for all $a, b \in \alpha$, then $\alpha$ inherits a generalized Boolean algebra structure from $\beta$ via $f$.
Function.Injective.booleanAlgebra abbrev
[Max α] [Min α] [Top α] [Bot α] [HasCompl α] [SDiff α] [HImp α] [BooleanAlgebra β] (f : α → β) (hf : 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) (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) : BooleanAlgebra α
Full source 
/-- Pullback a `BooleanAlgebra` along an injection. -/
protected abbrev Function.Injective.booleanAlgebra [Max α] [Min α] [Top α] [Bot α] [HasCompl α]
    [SDiff α] [HImp α] [BooleanAlgebra β] (f : α → β) (hf : 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) (map_himp : ∀ a b, f (a ⇨ b) = f a ⇨ f b) :
    BooleanAlgebra α where
  __ := hf.generalizedBooleanAlgebra f map_sup map_inf map_bot map_sdiff
  compl := compl
  himp := himp
  top := ⊤
  le_top _ := (@le_top β _ _ _).trans map_top.ge
  bot_le _ := map_bot.le.trans bot_le
  inf_compl_le_bot a := ((map_inf _ _).trans <| by rw [map_compl, inf_compl_eq_bot, map_bot]).le
  top_le_sup_compl a := ((map_sup _ _).trans <| by rw [map_compl, sup_compl_eq_top, map_top]).ge
  sdiff_eq a b := by
    refine hf ((map_sdiff _ _).trans (sdiff_eq.trans ?_))
    rw [map_inf, map_compl]
  himp_eq a b := hf <| (map_himp _ _).trans <| himp_eq.trans <| by rw [map_sup, map_compl]
Pullback of Boolean Algebra Structure Along an Injective Homomorphism
Informal description
Let $\alpha$ and $\beta$ be types equipped with lattice structures, where $\beta$ is a Boolean algebra. Given an injective function $f \colon \alpha \to \beta$ that preserves: - Suprema: $f(a \sqcup b) = f(a) \sqcup f(b)$ for all $a, b \in \alpha$, - Infima: $f(a \sqcap b) = f(a) \sqcap f(b)$ for all $a, b \in \alpha$, - Top element: $f(\top) = \top$, - Bottom element: $f(\bot) = \bot$, - Complement: $f(a^\complement) = (f(a))^\complement$ for all $a \in \alpha$, - Relative complement: $f(a \setminus b) = f(a) \setminus f(b)$ for all $a, b \in \alpha$, - Heyting implication: $f(a \Rightarrow b) = f(a) \Rightarrow f(b)$ for all $a, b \in \alpha$, then $\alpha$ inherits a Boolean algebra structure from $\beta$ via $f$.
PUnit.instBooleanAlgebra instance
: BooleanAlgebra PUnit
Full source 
instance PUnit.instBooleanAlgebra : BooleanAlgebra PUnit where
  __ := PUnit.instBiheytingAlgebra
  le_sup_inf := by simp
  inf_compl_le_bot _ := trivial
  top_le_sup_compl _ := trivial
Boolean Algebra Structure on the Trivial Type
Informal description
The trivial type `PUnit` (the type with a single element) has a canonical Boolean algebra structure, where all operations (meet, join, complement, set difference, and Heyting implication) are defined in the trivial way.
DistribLattice.booleanAlgebraOfComplemented definition
[BoundedOrder α] [ComplementedLattice α] : BooleanAlgebra α
Full source 
/--
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.
-/
noncomputable
def booleanAlgebraOfComplemented [BoundedOrder α] [ComplementedLattice α] : BooleanAlgebra α where
  __ := (inferInstanceAs (BoundedOrder α))
  compl a := Classical.choose <| exists_isCompl a
  inf_compl_le_bot a := (Classical.choose_spec (exists_isCompl a)).disjoint.le_bot
  top_le_sup_compl a := (Classical.choose_spec (exists_isCompl a)).codisjoint.top_le
Boolean algebra structure on a complemented distributive lattice
Informal description
Given a bounded distributive lattice $\alpha$ where every element has a complement (i.e., $\alpha$ is a complemented lattice), the structure $\alpha$ can be endowed with a Boolean algebra structure. The complement operation is defined using the axiom of choice to select a complement for each element, and the Boolean algebra axioms are satisfied: 1. For any element $a \in \alpha$, the infimum of $a$ and its complement is the bottom element $\bot$. 2. For any element $a \in \alpha$, the supremum of $a$ and its complement is the top element $\top$.