Boolean algebra on ZFSet

This file defines the boolean algebra on ZFSet and the type of booleans ZFBool. It defines the following operations:

• not : negation
• and : conjunction
• or : disjunction
• true : ZF true value
• false : ZF false value
• 𝔹 : set of ZF booleans
• toBool : conversion from ZFBool to Bool
• ofBool : conversion from Bool to ZFBool

Preliminary definitions

def ZFSet.symmDiff (p q : ZFSet.{u_1}) : ZFSet.{u_1}

Symmetric difference of two sets, denoted by Δ.

Equations

• p Δ q = p \ q ∪ q \ p

def ZFSet.term_Δ_ : Lean.TrailingParserDescr

Imported ZFLean declaration.

Equations

• ZFSet.term_Δ_ = Lean.ParserDescr.trailingNode `ZFSet.term_Δ_ 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " Δ ") (Lean.ParserDescr.cat `term 71))

@[simp]

theorem ZFSet.mem_symmDiff (x p q : ZFSet.{u_1}) : x ∈ p Δ q ↔ x ∈ p ∧ x ∉ q ∨ x ∈ q ∧ x ∉ p

@[simp]

theorem ZFSet.symmDiff_empty (p : ZFSet.{u_1}) : p Δ ∅ = p

theorem ZFSet.symmDiff_comm (p q : ZFSet.{u_1}) : p Δ q = q Δ p

@[simp]

theorem ZFSet.symmDiff_self (p : ZFSet.{u_1}) : p Δ p = ∅

ZF Boolean Algebra

@[reducible, inline]

abbrev ZFSet.zffalse : ZFSet.{u_1}

False value defined as the empty set.

Equations

• ZFSet.zffalse = ∅

@[reducible, inline]

abbrev ZFSet.zftrue : ZFSet.{u_1}

True value defined as the singleton containing the empty set.

Equations

• ZFSet.zftrue = {ZFSet.zffalse}

@[reducible, inline]

abbrev ZFSet.𝔹 : ZFSet.{u_1}

Set of ZF booleans, defined as the set containing zffalse and zftrue.

Equations

• ZFSet.𝔹 = {ZFSet.zffalse, ZFSet.zftrue}

@[reducible, inline]

abbrev ZFSet.ZFBool : Type (u_1 + 1)

Type of ZF booleans.

Equations

• ZFSet.ZFBool = ↥ZFSet.𝔹

theorem ZFSet.zftrue_ne_zffalse : zftrue ≠ zffalse

theorem ZFSet.ZFBool.zftrue_mem_𝔹 : zftrue ∈ 𝔹

theorem ZFSet.ZFBool.zffalse_mem_𝔹 : zffalse ∈ 𝔹

theorem ZFSet.ZFBool.𝔹.nonempty : 𝔹 ≠ ∅

@[reducible, inline]

abbrev ZFSet.ZFBool.false : ZFBool

False value, lifted on ZFBool.

Equations

• ZFSet.ZFBool.false = ⟨ZFSet.zffalse, ZFSet.ZFBool.zffalse_mem_𝔹⟩

@[reducible, inline]

abbrev ZFSet.ZFBool.true : ZFBool

True value, lifted on ZFBool.

Equations

• ZFSet.ZFBool.true = ⟨ZFSet.zftrue, ZFSet.ZFBool.zftrue_mem_𝔹⟩

@[implicit_reducible]

instance ZFSet.ZFBool.BoolTop : Top ZFBool

Equations

• ZFSet.ZFBool.BoolTop = { top := ZFSet.ZFBool.true }

@[implicit_reducible]

instance ZFSet.ZFBool.BoolBot : Bot ZFBool

Equations

• ZFSet.ZFBool.BoolBot = { bot := ZFSet.ZFBool.false }

theorem ZFSet.ZFBool.top_eq_true : ⊤ = true

@[simp]

theorem ZFSet.ZFBool.bot_eq_false : ⊥ = false

theorem ZFSet.ZFBool.true_ne_false : ⊤ ≠ ⊥

theorem ZFSet.ZFBool.mem_𝔹_iff (p : ZFSet.{u_1}) : p ∈ 𝔹 ↔ p = zffalse ∨ p = zftrue

@[simp]

theorem ZFSet.ZFBool.powerset_false : zffalse.powerset = zftrue

theorem ZFSet.ZFBool.powerset_𝔹_def : 𝔹.powerset = {∅, {zffalse}, {zftrue}, {zffalse, zftrue}}

The enumeration of the powerset of 𝔹.

@[reducible, inline]

abbrev ZFSet.ZFBool.not (p : ZFBool) : ZFBool

Boolean negation, defined as the symmetric difference with true.

Equations

• p.not = ⟨↑ZFSet.ZFBool.true Δ ↑p, ⋯⟩

noncomputable def ZFSet.ZFBool.casesOn {motive : ZFBool → Sort u_2} (p : ZFBool) (false : motive ⊥) (true : motive ⊤) : motive p

Cases elimination for ZFBool.

Equations

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

@[reducible, inline]

abbrev ZFSet.ZFBool.and (p q : ZFBool) : ZFBool

Boolean conjunction, defined as set intersection.

Equations

• ⟨Q, hQ⟩ ⋀ ⟨Q_1, hQ_1⟩ = ⟨Q ∩ Q_1, ⋯⟩

def ZFSet.ZFBool.«term_⋀_» : Lean.TrailingParserDescr

Imported ZFLean declaration.

Equations

• ZFSet.ZFBool.«term_⋀_» = Lean.ParserDescr.trailingNode `ZFSet.ZFBool.«term_⋀_» 55 55 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋀ ") (Lean.ParserDescr.cat `term 56))

@[reducible, inline]

abbrev ZFSet.ZFBool.or (p q : ZFBool) : ZFBool

Imported ZFLean declaration.

Equations

• ⟨Q, hQ⟩ ⋁ ⟨Q_1, hQ_1⟩ = ⟨Q ∪ Q_1, ⋯⟩

def ZFSet.ZFBool.«term_⋁_» : Lean.TrailingParserDescr

Imported ZFLean declaration.

Equations

• ZFSet.ZFBool.«term_⋁_» = Lean.ParserDescr.trailingNode `ZFSet.ZFBool.«term_⋁_» 55 55 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋁ ") (Lean.ParserDescr.cat `term 56))

Boolean algebra

theorem ZFSet.ZFBool.not_true_eq_false : ⊤.not = ⊥

theorem ZFSet.ZFBool.not_false_eq_true : ⊥.not = ⊤

theorem ZFSet.ZFBool.and_comm (p q : ZFBool) : p ⋀ q = q ⋀ p

theorem ZFSet.ZFBool.and_assoc (p q r : ZFBool) : p ⋀ q ⋀ r = p ⋀ (q ⋀ r)

theorem ZFSet.ZFBool.and_true (p : ZFBool) : p ⋀ ⊤ = p

@[simp]

theorem ZFSet.ZFBool.and_false (p : ZFBool) : p ⋀ ⊥ = ⊥

theorem ZFSet.ZFBool.and_iff (p q : ZFBool) : p ⋀ q = ⊤ ↔ p = ⊤ ∧ q = ⊤

theorem ZFSet.ZFBool.and_intro (p q : ZFBool) : p = ⊤ ∧ q = ⊤ → p ⋀ q = ⊤

theorem ZFSet.ZFBool.or_comm (p q : ZFBool) : p ⋁ q = q ⋁ p

theorem ZFSet.ZFBool.or_assoc (p q r : ZFBool) : p ⋁ q ⋁ r = p ⋁ (q ⋁ r)

theorem ZFSet.ZFBool.or_true (p : ZFBool) : p ⋁ ⊤ = ⊤

theorem ZFSet.ZFBool.or_false (p : ZFBool) : p ⋁ ⊥ = p

theorem ZFSet.ZFBool.or_iff (p q : ZFBool) : p ⋁ q = ⊤ ↔ p = ⊤ ∨ q = ⊤

theorem ZFSet.ZFBool.or_intro (p q : ZFBool) : p = ⊤ ∨ q = ⊤ → p ⋁ q = ⊤

noncomputable def ZFSet.ZFBool.toBool : ZFBool → Bool

Conversion of ZFBool to Lean.Bool.

Equations

• ZFSet.ZFBool.toBool ⟨Q, hQ⟩ = if h : Q = ZFSet.zftrue then true else if h' : Q = ZFSet.zffalse then false else ⋯.elim

theorem ZFSet.ZFBool.toBool_false : ⊥.toBool = Bool.false

theorem ZFSet.ZFBool.toBool_true : ⊤.toBool = Bool.true

theorem ZFSet.ZFBool.toBool_and (p q : ZFBool) : (p ⋀ q).toBool = (p.toBool && q.toBool)

theorem ZFSet.ZFBool.toBool_or (p q : ZFBool) : (p ⋁ q).toBool = (p.toBool || q.toBool)

theorem ZFSet.ZFBool.toBool_not (p : ZFBool) : (p.not.toBool = Bool.true) = ¬p.toBool = Bool.true

theorem ZFSet.ZFBool.not_top_iff_bot {P : ZFBool} : P ≠ ⊤ ↔ P = ⊥

theorem ZFSet.ZFBool.not_bot_iff_top {P : ZFBool} : P ≠ ⊥ ↔ P = ⊤

def ZFSet.ZFBool.ofBool : Bool → ZFBool

Conversion of Lean.Bool to ZFBool

Equations

• ZFSet.ZFBool.ofBool true = ⟨ZFSet.zftrue, ZFSet.ZFBool.zftrue_mem_𝔹⟩
• ZFSet.ZFBool.ofBool false = ⟨ZFSet.zffalse, ZFSet.ZFBool.zffalse_mem_𝔹⟩

theorem ZFSet.ZFBool.mem_ofBool_𝔹 (b : Bool) : ↑(ofBool b) ∈ 𝔹

theorem ZFSet.ZFBool.sub_ofBool_singleton_𝔹 (b : Bool) : {↑(ofBool b)} ⊆ 𝔹

theorem ZFSet.ZFBool.to_Bool_ofBool (b : Bool) : (ofBool b).toBool = b

theorem ZFSet.ZFBool.of_Bool_toBool (b : ZFBool) : ofBool b.toBool = b

theorem ZFSet.ZFBool.ofBool_decide_eq_true_iff {P : Prop} [Decidable P] : ofBool (decide P) = ⊤ ↔ P

theorem ZFSet.ZFBool.ofBool_decide_eq_false_iff {P : Prop} [Decidable P] : ofBool (decide P) = ⊥ ↔ ¬P

noncomputable def ZFSet.ZFBool.instEquivBool : ZFBool ≃ Bool

The equivalence between ZF booleans and Lean booleans.

Equations

• ZFSet.ZFBool.instEquivBool = { toFun := ZFSet.ZFBool.toBool, invFun := ZFSet.ZFBool.ofBool, left_inv := ZFSet.ZFBool.of_Bool_toBool, right_inv := ZFSet.ZFBool.to_Bool_ofBool }

@[implicit_reducible]

instance ZFSet.ZFBool.instCoeBool : Coe Bool ZFBool

Equations

• ZFSet.ZFBool.instCoeBool = { coe := ZFSet.ZFBool.ofBool }

@[implicit_reducible]

noncomputable instance ZFSet.ZFBool.instCoeBool_1 : Coe ZFBool Bool

Equations

• ZFSet.ZFBool.instCoeBool_1 = { coe := ZFSet.ZFBool.toBool }

theorem ZFSet.ZFBool.and_coe (p q : ZFBool) : p ⋀ q = ofBool (p.toBool && q.toBool)

theorem ZFSet.ZFBool.or_coe (p q : ZFBool) : p ⋁ q = ofBool (p.toBool || q.toBool)

theorem ZFSet.ZFBool.not_coe (p : ZFBool) : (p.not.toBool = Bool.true) = ¬p.toBool = Bool.true

theorem ZFSet.ZFBool.and_or_distrib_left (p q r : ZFBool) : p ⋀ (q ⋁ r) = p ⋀ q ⋁ (p ⋀ r)