@[reducible, inline]

abbrev LO.Axioms.Verum {F : Type u_1} [LO.LogicalConnective F] : F

Equations

• LO.Axioms.Verum = ⊤

@[reducible, inline]

abbrev LO.Axioms.Verum.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.Verum.set = {LO.Axioms.Verum}

@[reducible, inline]

abbrev LO.Axioms.Imply₁ {F : Type u_1} [LO.LogicalConnective F] (p : F) (q : F) : F

Equations

• LO.Axioms.Imply₁ p q = p ➝ q ➝ p

@[reducible, inline]

abbrev LO.Axioms.Imply₁.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.Imply₁.set = {x : F | ∃ (p : F) (q : F), LO.Axioms.Imply₁ p q = x}

@[reducible, inline]

abbrev LO.Axioms.Imply₂ {F : Type u_1} [LO.LogicalConnective F] (p : F) (q : F) (r : F) : F

Equations

• LO.Axioms.Imply₂ p q r = (p ➝ q ➝ r) ➝ (p ➝ q) ➝ p ➝ r

@[reducible, inline]

abbrev LO.Axioms.Imply₂.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.Imply₂.set = {x : F | ∃ (p : F) (q : F) (r : F), LO.Axioms.Imply₂ p q r = x}

@[reducible, inline]

abbrev LO.Axioms.ElimContra {F : Type u_1} [LO.LogicalConnective F] (p : F) (q : F) : F

Equations

• LO.Axioms.ElimContra p q = (∼q ➝ ∼p) ➝ p ➝ q

@[reducible, inline]

abbrev LO.Axioms.ElimContra.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.ElimContra.set = {x : F | ∃ (p : F) (q : F), LO.Axioms.ElimContra p q = x}

@[reducible, inline]

abbrev LO.Axioms.AndElim₁ {F : Type u_1} [LO.LogicalConnective F] (p : F) (q : F) : F

Equations

• LO.Axioms.AndElim₁ p q = p ⋏ q ➝ p

@[reducible, inline]

abbrev LO.Axioms.AndElim₁.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.AndElim₁.set = {x : F | ∃ (p : F) (q : F), LO.Axioms.AndElim₁ p q = x}

@[reducible, inline]

abbrev LO.Axioms.AndElim₂ {F : Type u_1} [LO.LogicalConnective F] (p : F) (q : F) : F

Equations

• LO.Axioms.AndElim₂ p q = p ⋏ q ➝ q

@[reducible, inline]

abbrev LO.Axioms.AndElim₂.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.AndElim₂.set = {x : F | ∃ (p : F) (q : F), LO.Axioms.AndElim₂ p q = x}

@[reducible, inline]

abbrev LO.Axioms.AndInst {F : Type u_1} [LO.LogicalConnective F] (p : F) (q : F) : F

Equations

• LO.Axioms.AndInst p q = p ➝ q ➝ p ⋏ q

@[reducible, inline]

abbrev LO.Axioms.AndInst.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.AndInst.set = {x : F | ∃ (p : F) (q : F), LO.Axioms.AndInst p q = x}

@[reducible, inline]

abbrev LO.Axioms.OrInst₁ {F : Type u_1} [LO.LogicalConnective F] (p : F) (q : F) : F

Equations

• LO.Axioms.OrInst₁ p q = p ➝ p ⋎ q

@[reducible, inline]

abbrev LO.Axioms.OrInst₁.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.OrInst₁.set = {x : F | ∃ (p : F) (q : F), LO.Axioms.OrInst₁ p q = x}

@[reducible, inline]

abbrev LO.Axioms.OrInst₂ {F : Type u_1} [LO.LogicalConnective F] (p : F) (q : F) : F

Equations

• LO.Axioms.OrInst₂ p q = q ➝ p ⋎ q

@[reducible, inline]

abbrev LO.Axioms.OrInst₂.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.OrInst₂.set = {x : F | ∃ (p : F) (q : F), LO.Axioms.OrInst₂ p q = x}

@[reducible, inline]

abbrev LO.Axioms.OrElim {F : Type u_1} [LO.LogicalConnective F] (p : F) (q : F) (r : F) : F

Equations

• LO.Axioms.OrElim p q r = (p ➝ r) ➝ (q ➝ r) ➝ p ⋎ q ➝ r

@[reducible, inline]

abbrev LO.Axioms.OrElim.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.OrElim.set = {x : F | ∃ (p : F) (q : F) (r : F), LO.Axioms.OrElim p q r = x}

@[reducible, inline]

abbrev LO.Axioms.NegEquiv {F : Type u_1} [LO.LogicalConnective F] (p : F) : F

Equations

• LO.Axioms.NegEquiv p = ∼p ⭤ (p ➝ ⊥)

@[reducible, inline]

abbrev LO.Axioms.NegEquiv.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• LO.Axioms.NegEquiv.set = {x : F | ∃ (p : F), LO.Axioms.NegEquiv p = x}

@[reducible, inline]

abbrev LO.Axioms.EFQ {F : Type u_1} [LO.LogicalConnective F] (p : F) : F

Equations

• LO.Axioms.EFQ p = ⊥ ➝ p

@[reducible, inline]

abbrev LO.Axioms.EFQ.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• 𝗘𝗙𝗤 = {x : F | ∃ (p : F), LO.Axioms.EFQ p = x}

def LO.Axioms.«term𝗘𝗙𝗤» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗘𝗙𝗤» = Lean.ParserDescr.node `LO.Axioms.term𝗘𝗙𝗤 1024 (Lean.ParserDescr.symbol "𝗘𝗙𝗤")

@[reducible, inline]

abbrev LO.Axioms.LEM {F : Type u_1} [LO.LogicalConnective F] (p : F) : F

Equations

• LO.Axioms.LEM p = p ⋎ ∼p

@[reducible, inline]

abbrev LO.Axioms.LEM.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• 𝗟𝗘𝗠 = {x : F | ∃ (p : F), LO.Axioms.LEM p = x}

def LO.Axioms.«term𝗟𝗘𝗠» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗟𝗘𝗠» = Lean.ParserDescr.node `LO.Axioms.term𝗟𝗘𝗠 1024 (Lean.ParserDescr.symbol "𝗟𝗘𝗠")

@[reducible, inline]

abbrev LO.Axioms.WeakLEM {F : Type u_1} [LO.LogicalConnective F] (p : F) : F

Equations

• LO.Axioms.WeakLEM p = ∼p ⋎ ∼∼p

@[reducible, inline]

abbrev LO.Axioms.WeakLEM.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• 𝗪𝗟𝗘𝗠 = {x : F | ∃ (p : F), LO.Axioms.WeakLEM p = x}

def LO.Axioms.«term𝗪𝗟𝗘𝗠» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗪𝗟𝗘𝗠» = Lean.ParserDescr.node `LO.Axioms.term𝗪𝗟𝗘𝗠 1024 (Lean.ParserDescr.symbol "𝗪𝗟𝗘𝗠")

@[reducible, inline]

abbrev LO.Axioms.GD {F : Type u_1} [LO.LogicalConnective F] (p : F) (q : F) : F

Equations

• LO.Axioms.GD p q = (p ➝ q) ⋎ (q ➝ p)

@[reducible, inline]

abbrev LO.Axioms.GD.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• 𝗗𝘂𝗺 = {x : F | ∃ (p : F) (q : F), LO.Axioms.GD p q = x}

def LO.Axioms.«term𝗗𝘂𝗺» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗗𝘂𝗺» = Lean.ParserDescr.node `LO.Axioms.term𝗗𝘂𝗺 1024 (Lean.ParserDescr.symbol "𝗗𝘂𝗺")

@[reducible, inline]

abbrev LO.Axioms.DNE {F : Type u_1} [LO.LogicalConnective F] (p : F) : F

Equations

• LO.Axioms.DNE p = ∼∼p ➝ p

@[reducible, inline]

abbrev LO.Axioms.DNE.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• 𝗗𝗡𝗘 = {x : F | ∃ (p : F), LO.Axioms.DNE p = x}

def LO.Axioms.«term𝗗𝗡𝗘» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗗𝗡𝗘» = Lean.ParserDescr.node `LO.Axioms.term𝗗𝗡𝗘 1024 (Lean.ParserDescr.symbol "𝗗𝗡𝗘")

@[reducible, inline]

abbrev LO.Axioms.Peirce {F : Type u_1} [LO.LogicalConnective F] (p : F) (q : F) : F

Equations

• LO.Axioms.Peirce p q = ((p ➝ q) ➝ p) ➝ p

@[reducible, inline]

abbrev LO.Axioms.Peirce.set {F : Type u_1} [LO.LogicalConnective F] : Set F

Equations

• 𝗣𝗲 = {x : F | ∃ (p : F) (q : F), LO.Axioms.Peirce p q = x}

def LO.Axioms.«term𝗣𝗲» : Lean.ParserDescr

Equations

• LO.Axioms.«term𝗣𝗲» = Lean.ParserDescr.node `LO.Axioms.term𝗣𝗲 1024 (Lean.ParserDescr.symbol "𝗣𝗲")