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]⊥, 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≤ b, the equations x ⊔ a = b⊔ a = b and x ⊓ a = ⊥⊓ a = ⊥⊥ have a solution x. disjoint.sdiff_unique proves that this x is in fact b \ a.

References #

https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#Generalizations
[Postulates for Boolean Algebras and Generalized Boolean Algebras, M.H. Stone][Stone1935]
[Lattice Theory: Foundation, George Grätzer][Gratzer2011]

Tags #

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

Generalized Boolean algebras #

Some of the lemmas in this section are from:

[Lattice Theory: Foundation, George Grätzer][Gratzer2011]
https://ncatlab.org/nlab/show/relative+complement
https://people.math.gatech.edu/~mccuan/courses/4317/symmetricdifference.pdf

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

For any a, b, (a ⊓ b) ⊔ (a / b) = a⊓ b) ⊔ (a / b) = a⊔ (a / b) = a
sup_inf_sdiff : ∀ (a b : α), a ⊓ b ⊔ a \ b = a
For any a, b, (a ⊓ b) ⊓ (a / b) = ⊥⊓ b) ⊓ (a / b) = ⊥⊓ (a / b) = ⊥⊥
inf_inf_sdiff : ∀ (a b : α), a ⊓ b ⊓ a \ b = ⊥

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⊓ b) ⊔ (a \ b) = a⊔ (a \ b) = a and (a ⊓ b) ⊓ (a \ b) = ⊥⊓ b) ⊓ (a \ b) = ⊥⊓ (a \ b) = ⊥⊥, i.e. a \ b is the complement of b in a.

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

Instances

@[simp]

theorem sup_inf_sdiff {α : Type u} [inst : GeneralizedBooleanAlgebra α] (x : α) (y : α) :

x ⊓ y ⊔ x \ y = x

@[simp]

theorem inf_inf_sdiff {α : Type u} [inst : GeneralizedBooleanAlgebra α] (x : α) (y : α) :

x ⊓ y ⊓ x \ y = ⊥

@[simp]

theorem sup_sdiff_inf {α : Type u} [inst : GeneralizedBooleanAlgebra α] (x : α) (y : α) :

x \ y ⊔ x ⊓ y = x

@[simp]

theorem inf_sdiff_inf {α : Type u} [inst : GeneralizedBooleanAlgebra α] (x : α) (y : α) :

x \ y ⊓ (x ⊓ y) = ⊥

instance GeneralizedBooleanAlgebra.toOrderBot {α : Type u} [inst : GeneralizedBooleanAlgebra α] :

Equations

GeneralizedBooleanAlgebra.toOrderBot = let src := GeneralizedBooleanAlgebra.toBot; OrderBot.mk (_ : ∀ (a : α), ⊥ ≤ a)

theorem disjoint_inf_sdiff {α : Type u} {x : α} {y : α} [inst : GeneralizedBooleanAlgebra α] :

Disjoint (x ⊓ y) (x \ y)

theorem sdiff_unique {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] (s : x ⊓ y ⊔ z = x) (i : x ⊓ y ⊓ z = ⊥) :

x \ y = z

@[simp]

theorem sdiff_inf_sdiff {α : Type u} {x : α} {y : α} [inst : GeneralizedBooleanAlgebra α] :

x \ y ⊓ y \ x = ⊥

theorem disjoint_sdiff_sdiff {α : Type u} {x : α} {y : α} [inst : GeneralizedBooleanAlgebra α] :

Disjoint (x \ y) (y \ x)

@[simp]

theorem inf_sdiff_self_right {α : Type u} {x : α} {y : α} [inst : GeneralizedBooleanAlgebra α] :

x ⊓ y \ x = ⊥

@[simp]

theorem inf_sdiff_self_left {α : Type u} {x : α} {y : α} [inst : GeneralizedBooleanAlgebra α] :

y \ x ⊓ x = ⊥

instance GeneralizedBooleanAlgebra.toGeneralizedCoheytingAlgebra {α : Type u} [inst : GeneralizedBooleanAlgebra α] :

GeneralizedCoheytingAlgebra α

Equations

One or more equations did not get rendered due to their size.

theorem disjoint_sdiff_self_left {α : Type u} {x : α} {y : α} [inst : GeneralizedBooleanAlgebra α] :

Disjoint (y \ x) x

theorem disjoint_sdiff_self_right {α : Type u} {x : α} {y : α} [inst : GeneralizedBooleanAlgebra α] :

Disjoint x (y \ x)

theorem le_sdiff {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] :

x ≤ y \ z ↔ x ≤ y ∧ Disjoint x z

@[simp]

theorem sdiff_eq_left {α : Type u} {x : α} {y : α} [inst : GeneralizedBooleanAlgebra α] :

x \ y = x ↔ Disjoint x y

theorem Disjoint.sdiff_eq_of_sup_eq {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] (hi : Disjoint x z) (hs : x ⊔ z = y) :

y \ x = z

theorem Disjoint.sdiff_unique {α : Type u} {x : α} {y : α} {z : α} [inst : 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 : α} [inst : GeneralizedBooleanAlgebra α] (hz : z ≤ y) (hx : x ≤ y) :

Disjoint z (y \ x) ↔ z ≤ x

theorem le_iff_disjoint_sdiff {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] (hz : z ≤ y) (hx : x ≤ y) :

z ≤ x ↔ Disjoint z (y \ x)

theorem inf_sdiff_eq_bot_iff {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] (hz : z ≤ y) (hx : x ≤ y) :

z ⊓ y \ x = ⊥ ↔ z ≤ x

theorem le_iff_eq_sup_sdiff {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] (hz : z ≤ y) (hx : x ≤ y) :

x ≤ z ↔ y = z ⊔ y \ x

theorem sdiff_sup {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] :

y \ (x ⊔ z) = y \ x ⊓ y \ z

theorem sdiff_eq_sdiff_iff_inf_eq_inf {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] :

y \ x = y \ z ↔ y ⊓ x = y ⊓ z

theorem sdiff_eq_self_iff_disjoint {α : Type u} {x : α} {y : α} [inst : GeneralizedBooleanAlgebra α] :

x \ y = x ↔ Disjoint y x

theorem sdiff_eq_self_iff_disjoint' {α : Type u} {x : α} {y : α} [inst : GeneralizedBooleanAlgebra α] :

x \ y = x ↔ Disjoint x y

theorem sdiff_lt {α : Type u} {x : α} {y : α} [inst : GeneralizedBooleanAlgebra α] (hx : y ≤ x) (hy : y ≠ ⊥) :

x \ y < x

@[simp]

theorem le_sdiff_iff {α : Type u} {x : α} {y : α} [inst : GeneralizedBooleanAlgebra α] :

x ≤ y \ x ↔ x = ⊥

theorem sdiff_lt_sdiff_right {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] (h : x < y) (hz : z ≤ x) :

x \ z < y \ z

theorem sup_inf_inf_sdiff {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] :

x ⊓ y ⊓ z ⊔ y \ z = x ⊓ y ⊔ y \ z

theorem sdiff_sdiff_right {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] :

x \ (y \ z) = x \ y ⊔ x ⊓ y ⊓ z

theorem sdiff_sdiff_right' {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] :

x \ (y \ z) = x \ y ⊔ x ⊓ z

theorem sdiff_sdiff_eq_sdiff_sup {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] (h : z ≤ x) :

x \ (y \ z) = x \ y ⊔ z

@[simp]

theorem sdiff_sdiff_right_self {α : Type u} {x : α} {y : α} [inst : GeneralizedBooleanAlgebra α] :

x \ (x \ y) = x ⊓ y

theorem sdiff_sdiff_eq_self {α : Type u} {x : α} {y : α} [inst : GeneralizedBooleanAlgebra α] (h : y ≤ x) :

x \ (x \ y) = y

theorem sdiff_eq_symm {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] (hy : y ≤ x) (h : x \ y = z) :

x \ z = y

theorem sdiff_eq_comm {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] (hy : y ≤ x) (hz : z ≤ x) :

x \ y = z ↔ x \ z = y

theorem eq_of_sdiff_eq_sdiff {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] (hxz : x ≤ z) (hyz : y ≤ z) (h : z \ x = z \ y) :

x = y

theorem sdiff_sdiff_left' {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] :

(x \ y) \ z = x \ y ⊓ x \ z

theorem sdiff_sdiff_sup_sdiff {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] :

z \ (x \ y ⊔ y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x)

theorem sdiff_sdiff_sup_sdiff' {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] :

z \ (x \ y ⊔ y \ x) = z ⊓ x ⊓ y ⊔ z \ x ⊓ z \ y

theorem inf_sdiff {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] :

(x ⊓ y) \ z = x \ z ⊓ y \ z

theorem inf_sdiff_assoc {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] :

(x ⊓ y) \ z = x ⊓ y \ z

theorem inf_sdiff_right_comm {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] :

x \ z ⊓ y = (x ⊓ y) \ z

theorem inf_sdiff_distrib_left {α : Type u} [inst : GeneralizedBooleanAlgebra α] (a : α) (b : α) (c : α) :

a ⊓ b \ c = (a ⊓ b) \ (a ⊓ c)

theorem inf_sdiff_distrib_right {α : Type u} [inst : GeneralizedBooleanAlgebra α] (a : α) (b : α) (c : α) :

a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c)

theorem sup_eq_sdiff_sup_sdiff_sup_inf {α : Type u} {x : α} {y : α} [inst : GeneralizedBooleanAlgebra α] :

x ⊔ y = x \ y ⊔ y \ x ⊔ x ⊓ y

theorem sup_lt_of_lt_sdiff_left {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] (h : y < z \ x) (hxz : x ≤ z) :

x ⊔ y < z

theorem sup_lt_of_lt_sdiff_right {α : Type u} {x : α} {y : α} {z : α} [inst : GeneralizedBooleanAlgebra α] (h : x < z \ y) (hyz : y ≤ z) :

x ⊔ y < z

instance Pi.generalizedBooleanAlgebra {α : Type u} {β : Type v} [inst : GeneralizedBooleanAlgebra β] :

GeneralizedBooleanAlgebra (α → β)

Equations

Pi.generalizedBooleanAlgebra = GeneralizedBooleanAlgebra.mk (_ : ∀ (f g : α → β), f ⊓ g ⊔ f \ g = f) (_ : ∀ (f g : α → β), f ⊓ g ⊓ f \ g = ⊥)

Boolean algebras #

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

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ᶜ⊓ yᶜ
sdiff_eq : autoParam (∀ (x y : α), x \ y = x ⊓ yᶜ) _auto✝
x ⇨ y⇨ y is equal to y ⊔ xᶜ⊔ xᶜ
himp_eq : autoParam (∀ (x y : α), x ⇨ y = y ⊔ xᶜ) _auto✝

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

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

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

Instances

instance BooleanAlgebra.toBoundedOrder {α : Type u} [h : BooleanAlgebra α] :

BoundedOrder α

Equations

BooleanAlgebra.toBoundedOrder = BoundedOrder.mk

def GeneralizedBooleanAlgebra.toBooleanAlgebra {α : Type u} [inst : GeneralizedBooleanAlgebra α] [inst : OrderTop α] :

BooleanAlgebra α

A bounded generalized boolean algebra is a boolean algebra.

Equations

One or more equations did not get rendered due to their size.

theorem inf_compl_eq_bot' {α : Type u} {x : α} [inst : BooleanAlgebra α] :

x ⊓ xᶜ = ⊥

@[simp]

theorem sup_compl_eq_top {α : Type u} {x : α} [inst : BooleanAlgebra α] :

x ⊔ xᶜ = ⊤

@[simp]

theorem compl_sup_eq_top {α : Type u} {x : α} [inst : BooleanAlgebra α] :

xᶜ ⊔ x = ⊤

theorem isCompl_compl {α : Type u} {x : α} [inst : BooleanAlgebra α] :

IsCompl x (xᶜ)

theorem sdiff_eq {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

x \ y = x ⊓ yᶜ

theorem himp_eq {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

x ⇨ y = y ⊔ xᶜ

instance BooleanAlgebra.toComplementedLattice {α : Type u} [inst : BooleanAlgebra α] :

ComplementedLattice α

Equations

@BooleanAlgebra.toComplementedLattice = @BooleanAlgebra.toComplementedLattice.proof_1

instance BooleanAlgebra.toGeneralizedBooleanAlgebra {α : Type u} [inst : BooleanAlgebra α] :

GeneralizedBooleanAlgebra α

Equations

BooleanAlgebra.toGeneralizedBooleanAlgebra = let src := inst; GeneralizedBooleanAlgebra.mk (_ : ∀ (a b : α), a ⊓ b ⊔ a \ b = a) (_ : ∀ (a b : α), a ⊓ b ⊓ a \ b = ⊥)

instance BooleanAlgebra.toBiheytingAlgebra {α : Type u} [inst : BooleanAlgebra α] :

BiheytingAlgebra α

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem hnot_eq_compl {α : Type u} {x : α} [inst : BooleanAlgebra α] :

theorem top_sdiff {α : Type u} {x : α} [inst : BooleanAlgebra α] :

theorem eq_compl_iff_isCompl {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

x = yᶜ ↔ IsCompl x y

theorem compl_eq_iff_isCompl {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

xᶜ = y ↔ IsCompl x y

theorem compl_eq_comm {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

xᶜ = y ↔ yᶜ = x

theorem eq_compl_comm {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

x = yᶜ ↔ y = xᶜ

@[simp]

theorem compl_compl {α : Type u} [inst : BooleanAlgebra α] (x : α) :

theorem compl_comp_compl {α : Type u} [inst : BooleanAlgebra α] :

compl ∘ compl = id

@[simp]

theorem compl_involutive {α : Type u} [inst : BooleanAlgebra α] :

Function.Involutive compl

theorem compl_bijective {α : Type u} [inst : BooleanAlgebra α] :

Function.Bijective compl

theorem compl_surjective {α : Type u} [inst : BooleanAlgebra α] :

Function.Surjective compl

theorem compl_injective {α : Type u} [inst : BooleanAlgebra α] :

Function.Injective compl

@[simp]

theorem compl_inj_iff {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

xᶜ = yᶜ ↔ x = y

theorem IsCompl.compl_eq_iff {α : Type u} {x : α} {y : α} {z : α} [inst : BooleanAlgebra α] (h : IsCompl x y) :

zᶜ = y ↔ z = x

@[simp]

theorem compl_eq_top {α : Type u} {x : α} [inst : BooleanAlgebra α] :

xᶜ = ⊤ ↔ x = ⊥

@[simp]

theorem compl_eq_bot {α : Type u} {x : α} [inst : BooleanAlgebra α] :

xᶜ = ⊥ ↔ x = ⊤

@[simp]

theorem compl_inf {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

(x ⊓ y)ᶜ = xᶜ ⊔ yᶜ

@[simp]

theorem compl_le_compl_iff_le {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

yᶜ ≤ xᶜ ↔ x ≤ y

theorem compl_le_of_compl_le {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] (h : yᶜ ≤ x) :

theorem compl_le_iff_compl_le {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

xᶜ ≤ y ↔ yᶜ ≤ x

@[simp]

theorem sdiff_compl {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

x \ yᶜ = x ⊓ y

instance instBooleanAlgebraOrderDual {α : Type u} [inst : BooleanAlgebra α] :

BooleanAlgebra αᵒᵈ

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem sup_inf_inf_compl {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

x ⊓ y ⊔ x ⊓ yᶜ = x

@[simp]

theorem compl_sdiff {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

(x \ y)ᶜ = x ⇨ y

@[simp]

theorem compl_himp {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

(x ⇨ y)ᶜ = x \ y

theorem compl_sdiff_compl {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

xᶜ \ yᶜ = y \ x

@[simp]

theorem compl_himp_compl {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

xᶜ ⇨ yᶜ = y ⇨ x

theorem disjoint_compl_left_iff {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

Disjoint (xᶜ) y ↔ y ≤ x

theorem disjoint_compl_right_iff {α : Type u} {x : α} {y : α} [inst : BooleanAlgebra α] :

Disjoint x (yᶜ) ↔ x ≤ y

instance Prop.booleanAlgebra :

BooleanAlgebra Prop

Equations

One or more equations did not get rendered due to their size.

instance Pi.booleanAlgebra {ι : Type u} {α : ι → Type v} [inst : (i : ι) → BooleanAlgebra (α i)] :

BooleanAlgebra ((i : ι) → α i)

Equations

One or more equations did not get rendered due to their size.

instance instBooleanAlgebraBool :

BooleanAlgebra Bool

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem Bool.sup_eq_bor :

(fun x x_1 => x ⊔ x_1) = or

@[simp]

theorem Bool.inf_eq_band :

(fun x x_1 => x ⊓ x_1) = and

@[simp]

theorem Bool.compl_eq_bnot :

compl = not

def Function.Injective.generalizedBooleanAlgebra {α : Type u} {β : Type u_1} [inst : Sup α] [inst : Inf α] [inst : Bot α] [inst : SDiff α] [inst : 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) :

GeneralizedBooleanAlgebra α

Pullback a GeneralizedBooleanAlgebra along an injection.

Equations

One or more equations did not get rendered due to their size.

def Function.Injective.booleanAlgebra {α : Type u} {β : Type u_1} [inst : Sup α] [inst : Inf α] [inst : Top α] [inst : Bot α] [inst : HasCompl α] [inst : SDiff α] [inst : 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) :

BooleanAlgebra α

Pullback a BooleanAlgebra along an injection.

Equations

One or more equations did not get rendered due to their size.

instance PUnit.booleanAlgebra :

BooleanAlgebra PUnit

Equations

PUnit.booleanAlgebra = let src := PUnit.biheytingAlgebra; BooleanAlgebra.mk PUnit.booleanAlgebra.proof_2 PUnit.booleanAlgebra.proof_3 PUnit.booleanAlgebra.proof_4 PUnit.booleanAlgebra.proof_5