Logic Symbols

This file defines structure that has logical connectives $\top, \bot, \land, \lor, \to, \lnot$ and their homomorphisms.

Main Definitions

• LO.LogicalConnective is defined so that LO.LogicalConnective F is a type that has logical connectives $\top, \bot, \land, \lor, \to, \lnot$.
• LO.LogicalConnective.Hom is defined so that f : F →ˡᶜ G is a homomorphism from F to G, i.e., a function that preserves logical connectives.

class LO.SigmaSymbol (α : Type u_1) : Type u_1

• sigma : α

class LO.PiSymbol (α : Type u_1) : Type u_1

• pi : α

class LO.DeltaSymbol (α : Type u_1) : Type u_1

• delta : α

def LO.«term𝚺» : Lean.ParserDescr

Equations

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

def LO.«term𝚷» : Lean.ParserDescr

Equations

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

def LO.«term𝚫» : Lean.ParserDescr

Equations

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

inductive LO.Polarity : Type

• sigma: LO.Polarity
• pi: LO.Polarity

instance LO.Polarity.instSigmaSymbol : LO.SigmaSymbol LO.Polarity

Equations

• LO.Polarity.instSigmaSymbol = { sigma := LO.Polarity.sigma }

instance LO.Polarity.instPiSymbol : LO.PiSymbol LO.Polarity

Equations

• LO.Polarity.instPiSymbol = { pi := LO.Polarity.pi }

def LO.Polarity.alt : LO.Polarity → LO.Polarity

Equations

• x.alt = match x with | LO.Polarity.sigma => 𝚷 | LO.Polarity.pi => 𝚺

@[simp]

theorem LO.Polarity.eq_sigma : LO.Polarity.sigma = 𝚺

@[simp]

theorem LO.Polarity.eq_pi : LO.Polarity.pi = 𝚷

@[simp]

theorem LO.Polarity.alt_sigma : 𝚺.alt = 𝚷

@[simp]

theorem LO.Polarity.alt_pi : 𝚷.alt = 𝚺

@[simp]

theorem LO.Polarity.alt_alt (Γ : LO.Polarity) : Γ.alt.alt = Γ

inductive LO.SigmaPiDelta : Type

• sigma: LO.SigmaPiDelta
• pi: LO.SigmaPiDelta
• delta: LO.SigmaPiDelta

instance LO.SigmaPiDelta.instSigmaSymbol : LO.SigmaSymbol LO.SigmaPiDelta

Equations

• LO.SigmaPiDelta.instSigmaSymbol = { sigma := LO.SigmaPiDelta.sigma }

instance LO.SigmaPiDelta.instPiSymbol : LO.PiSymbol LO.SigmaPiDelta

Equations

• LO.SigmaPiDelta.instPiSymbol = { pi := LO.SigmaPiDelta.pi }

instance LO.SigmaPiDelta.instDeltaSymbol : LO.DeltaSymbol LO.SigmaPiDelta

Equations

• LO.SigmaPiDelta.instDeltaSymbol = { delta := LO.SigmaPiDelta.delta }

def LO.SigmaPiDelta.alt : LO.SigmaPiDelta → LO.SigmaPiDelta

Equations

• x.alt = match x with | LO.SigmaPiDelta.sigma => 𝚷 | LO.SigmaPiDelta.pi => 𝚺 | LO.SigmaPiDelta.delta => 𝚫

@[simp]

theorem LO.SigmaPiDelta.eq_sigma : LO.SigmaPiDelta.sigma = 𝚺

@[simp]

theorem LO.SigmaPiDelta.eq_pi : LO.SigmaPiDelta.pi = 𝚷

@[simp]

theorem LO.SigmaPiDelta.eq_delta : LO.SigmaPiDelta.delta = 𝚫

@[simp]

theorem LO.SigmaPiDelta.alt_sigma : 𝚺.alt = 𝚷

@[simp]

theorem LO.SigmaPiDelta.alt_pi : 𝚷.alt = 𝚺

@[simp]

theorem LO.SigmaPiDelta.alt_delta : 𝚫.alt = 𝚫

@[simp]

theorem LO.SigmaPiDelta.alt_alt (Γ : LO.SigmaPiDelta) : Γ.alt.alt = Γ

class LO.Tilde (α : Type u_1) : Type u_1

• tilde : α → α

class LO.Arrow (α : Type u_1) : Type u_1

• arrow : α → α → α

class LO.Wedge (α : Type u_1) : Type u_1

• wedge : α → α → α

class LO.Vee (α : Type u_1) : Type u_1

• vee : α → α → α

class LO.LogicalConnective (α : Type u_1) extends Top , Bot , LO.Tilde , LO.Arrow , LO.Wedge , LO.Vee : Type u_1

class LO.UnivQuantifier (α : ℕ → Type u_1) : Type u_1

• univ : {n : ℕ} → α (n + 1) → α n

class LO.ExQuantifier (α : ℕ → Type u_1) : Type u_1

• ex : {n : ℕ} → α (n + 1) → α n

class LO.UnivQuantifier₂ (α : ℕ → ℕ → Type u_1) : Type u_1

• univ₂₁ : {m n : ℕ} → α (m + 1) n → α m n
• univ₂₂ : {m n : ℕ} → α m (n + 1) → α m n

class LO.ExQuantifier₂ (α : ℕ → ℕ → Type u_1) : Type u_1

• ex₂₁ : {m n : ℕ} → α (m + 1) n → α m n
• ex₂₂ : {m n : ℕ} → α m (n + 1) → α m n

def LO.«term∼_» : Lean.ParserDescr

Equations

• LO.«term∼_» = Lean.ParserDescr.node `LO.term∼_ 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∼") (Lean.ParserDescr.cat `term 75))

def LO.«term_➝_» : Lean.TrailingParserDescr

Equations

• LO.«term_➝_» = Lean.ParserDescr.trailingNode `LO.term_➝_ 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ➝ ") (Lean.ParserDescr.cat `term 60))

def LO.«term_⋏_» : Lean.TrailingParserDescr

Equations

• LO.«term_⋏_» = Lean.ParserDescr.trailingNode `LO.term_⋏_ 69 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋏ ") (Lean.ParserDescr.cat `term 69))

def LO.«term_⋎_» : Lean.TrailingParserDescr

Equations

• LO.«term_⋎_» = Lean.ParserDescr.trailingNode `LO.term_⋎_ 68 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋎ ") (Lean.ParserDescr.cat `term 68))

def LO.«term∀'_» : Lean.ParserDescr

Equations

• LO.«term∀'_» = Lean.ParserDescr.node `LO.term∀'_ 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀' ") (Lean.ParserDescr.cat `term 64))

def LO.«term∃'_» : Lean.ParserDescr

Equations

• LO.«term∃'_» = Lean.ParserDescr.node `LO.term∃'_ 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∃' ") (Lean.ParserDescr.cat `term 64))

def LO.«term∀¹_» : Lean.ParserDescr

Equations

• LO.«term∀¹_» = Lean.ParserDescr.node `LO.term∀¹_ 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀¹ ") (Lean.ParserDescr.cat `term 64))

def LO.«term∀²_» : Lean.ParserDescr

Equations

• LO.«term∀²_» = Lean.ParserDescr.node `LO.term∀²_ 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀² ") (Lean.ParserDescr.cat `term 64))

def LO.«term∃¹_» : Lean.ParserDescr

Equations

• LO.«term∃¹_» = Lean.ParserDescr.node `LO.term∃¹_ 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∃¹ ") (Lean.ParserDescr.cat `term 64))

def LO.«term∃²_» : Lean.ParserDescr

Equations

• LO.«term∃²_» = Lean.ParserDescr.node `LO.term∃²_ 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∃² ") (Lean.ParserDescr.cat `term 64))

def LO.univClosure {α : ℕ → Type u_1} [LO.UnivQuantifier α] {n : ℕ} : α n → α 0

Equations

• ∀* a = a
• ∀* a = ∀* ∀' a

def LO.«term∀*_» : Lean.ParserDescr

Equations

• LO.«term∀*_» = Lean.ParserDescr.node `LO.term∀*_ 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∀* ") (Lean.ParserDescr.cat `term 64))

@[simp]

theorem LO.univClosure_zero {α : ℕ → Type u_1} [LO.UnivQuantifier α] (a : α 0) : ∀* a = a

theorem LO.univClosure_succ {α : ℕ → Type u_1} [LO.UnivQuantifier α] {n : ℕ} (a : α (n + 1)) : ∀* a = ∀* ∀' a

def LO.univItr {α : ℕ → Type u_1} [LO.UnivQuantifier α] {n : ℕ} (k : ℕ) : α (n + k) → α n

Equations

• ∀^[0] a = a
• ∀^[k.succ] a = ∀^[k] ∀' a

def LO.«term∀^[_]_» : Lean.ParserDescr

Equations

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

@[simp]

theorem LO.univItr_zero {α : ℕ → Type u_1} [LO.UnivQuantifier α] {n : ℕ} (a : α n) : ∀^[0] a = a

@[simp]

theorem LO.univItr_one {α : ℕ → Type u_1} [LO.UnivQuantifier α] {n : ℕ} (a : α (n + 1)) : ∀^[1] a = ∀' a

theorem LO.univItr_succ {α : ℕ → Type u_1} [LO.UnivQuantifier α] {n : ℕ} {k : ℕ} (a : α (n + (k + 1))) : ∀^[k + 1] a = ∀^[k] ∀' a

def LO.exClosure {α : ℕ → Type u_1} [LO.ExQuantifier α] {n : ℕ} : α n → α 0

Equations

• ∃* a = a
• ∃* a = ∃* ∃' a

def LO.«term∃*_» : Lean.ParserDescr

Equations

• LO.«term∃*_» = Lean.ParserDescr.node `LO.term∃*_ 64 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∃* ") (Lean.ParserDescr.cat `term 64))

@[simp]

theorem LO.exClosure_zero {α : ℕ → Type u_1} [LO.ExQuantifier α] (a : α 0) : ∃* a = a

theorem LO.exClosure_succ {α : ℕ → Type u_1} [LO.ExQuantifier α] {n : ℕ} (a : α (n + 1)) : ∃* a = ∃* ∃' a

def LO.exItr {α : ℕ → Type u_1} [LO.ExQuantifier α] {n : ℕ} (k : ℕ) : α (n + k) → α n

Equations

• ∃^[0] a = a
• ∃^[k.succ] a = ∃^[k] ∃' a

def LO.«term∃^[_]_» : Lean.ParserDescr

Equations

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

@[simp]

theorem LO.exItr_zero {α : ℕ → Type u_1} [LO.ExQuantifier α] {n : ℕ} (a : α n) : ∃^[0] a = a

@[simp]

theorem LO.exItr_one {α : ℕ → Type u_1} [LO.ExQuantifier α] {n : ℕ} (a : α (n + 1)) : ∃^[1] a = ∃' a

theorem LO.exItr_succ {α : ℕ → Type u_1} [LO.ExQuantifier α] {n : ℕ} {k : ℕ} (a : α (n + (k + 1))) : ∃^[k + 1] a = ∃^[k] ∃' a

def LO.quant {α : ℕ → Type u_1} [LO.UnivQuantifier α] [LO.ExQuantifier α] {n : ℕ} : LO.Polarity → α (n + 1) → α n

Equations

• LO.quant x✝ x = match x✝, x with | LO.Polarity.sigma, p => ∃' p | LO.Polarity.pi, p => ∀' p

@[simp]

theorem LO.quant_sigma {α : ℕ → Type u_1} [LO.UnivQuantifier α] [LO.ExQuantifier α] {n : ℕ} (p : α (n + 1)) : LO.quant 𝚺 p = ∃' p

@[simp]

theorem LO.quant_pi {α : ℕ → Type u_1} [LO.UnivQuantifier α] [LO.ExQuantifier α] {n : ℕ} (p : α (n + 1)) : LO.quant 𝚷 p = ∀' p

def LO.univClosure₂₁ {α : ℕ → ℕ → Type u_1} [LO.UnivQuantifier₂ α] {m : ℕ} {n : ℕ} : α m n → α 0 n

Equations

• LO.univClosure₂₁ x = x
• LO.univClosure₂₁ x = LO.univClosure₂₁ (∀¹ x)

def LO.univClosure₂₂ {α : ℕ → ℕ → Type u_1} [LO.UnivQuantifier₂ α] {m : ℕ} {n : ℕ} : α m n → α m 0

Equations

• LO.univClosure₂₂ a = a
• LO.univClosure₂₂ a = LO.univClosure₂₂ (∀² a)

@[simp]

theorem LO.univClosure₂₁_zero {α : ℕ → ℕ → Type u_1} [LO.UnivQuantifier₂ α] {n : ℕ} (a : α 0 n) : LO.univClosure₂₁ a = a

theorem LO.univClosure₂₁_succ {α : ℕ → ℕ → Type u_1} [LO.UnivQuantifier₂ α] {m : ℕ} {n : ℕ} (a : α (m + 1) n) : LO.univClosure₂₁ a = LO.univClosure₂₁ (∀¹ a)

@[simp]

theorem LO.univClosure₂₂_zero {α : ℕ → ℕ → Type u_1} [LO.UnivQuantifier₂ α] {m : ℕ} (a : α m 0) : LO.univClosure₂₂ a = a

theorem LO.univClosure₂₂_succ {α : ℕ → ℕ → Type u_1} [LO.UnivQuantifier₂ α] {m : ℕ} {n : ℕ} (a : α m (n + 1)) : LO.univClosure₂₂ a = LO.univClosure₂₂ (∀² a)

def LO.exClosure₂₁ {α : ℕ → ℕ → Type u_1} [LO.ExQuantifier₂ α] {m : ℕ} {n : ℕ} : α m n → α 0 n

Equations

• LO.exClosure₂₁ x = x
• LO.exClosure₂₁ x = LO.exClosure₂₁ (∃¹ x)

def LO.exClosure₂₂ {α : ℕ → ℕ → Type u_1} [LO.ExQuantifier₂ α] {m : ℕ} {n : ℕ} : α m n → α m 0

Equations

• LO.exClosure₂₂ a = a
• LO.exClosure₂₂ a = LO.exClosure₂₂ (∃² a)

@[simp]

theorem LO.exClosure₂₁_zero {α : ℕ → ℕ → Type u_1} [LO.ExQuantifier₂ α] {n : ℕ} (a : α 0 n) : LO.exClosure₂₁ a = a

theorem LO.exClosure₂₁_succ {α : ℕ → ℕ → Type u_1} [LO.ExQuantifier₂ α] {m : ℕ} {n : ℕ} (a : α (m + 1) n) : LO.exClosure₂₁ a = LO.exClosure₂₁ (∃¹ a)

@[simp]

theorem LO.exClosure₂₂_zero {α : ℕ → ℕ → Type u_1} [LO.ExQuantifier₂ α] {m : ℕ} (a : α m 0) : LO.exClosure₂₂ a = a

theorem LO.exClosure₂₂_succ {α : ℕ → ℕ → Type u_1} [LO.ExQuantifier₂ α] {m : ℕ} {n : ℕ} (a : α m (n + 1)) : LO.exClosure₂₂ a = LO.exClosure₂₂ (∃² a)

class LO.DeMorgan (F : Type u_1) [LO.LogicalConnective F] : Type

• verum : ∼⊤ = ⊥
• falsum : ∼⊥ = ⊤
• imply : ∀ (p q : F), p ➝ q = ∼p ⋎ q
• and : ∀ (p q : F), ∼(p ⋏ q) = ∼p ⋎ ∼q
• or : ∀ (p q : F), ∼(p ⋎ q) = ∼p ⋏ ∼q
• neg : ∀ (p : F), ∼∼p = p

@[simp]

theorem LO.DeMorgan.verum {F : Type u_1} [LO.LogicalConnective F] [self : LO.DeMorgan F] : ∼⊤ = ⊥

@[simp]

theorem LO.DeMorgan.falsum {F : Type u_1} [LO.LogicalConnective F] [self : LO.DeMorgan F] : ∼⊥ = ⊤

theorem LO.DeMorgan.imply {F : Type u_1} [LO.LogicalConnective F] [self : LO.DeMorgan F] (p : F) (q : F) : p ➝ q = ∼p ⋎ q

@[simp]

theorem LO.DeMorgan.and {F : Type u_1} [LO.LogicalConnective F] [self : LO.DeMorgan F] (p : F) (q : F) : ∼(p ⋏ q) = ∼p ⋎ ∼q

@[simp]

theorem LO.DeMorgan.or {F : Type u_1} [LO.LogicalConnective F] [self : LO.DeMorgan F] (p : F) (q : F) : ∼(p ⋎ q) = ∼p ⋏ ∼q

@[simp]

theorem LO.DeMorgan.neg {F : Type u_1} [LO.LogicalConnective F] [self : LO.DeMorgan F] (p : F) : ∼∼p = p

class LO.NegAbbrev (F : Type u_1) [LO.Tilde F] [LO.Arrow F] [Bot F] : Type

Introducing ∼p as an abbreviation of p ➝ ⊥.

• neg : ∀ {p : F}, ∼p = p ➝ ⊥

theorem LO.NegAbbrev.neg {F : Type u_1} [LO.Tilde F] [LO.Arrow F] [Bot F] [self : LO.NegAbbrev F] {p : F} : ∼p = p ➝ ⊥

@[match_pattern]

def LO.LogicalConnective.iff {α : Type u_1} [LO.LogicalConnective α] (a : α) (b : α) : α

Equations

• a ⭤ b = (a ➝ b) ⋏ (b ➝ a)

def LO.LogicalConnective.«term_⭤_» : Lean.TrailingParserDescr

Equations

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

@[reducible]

instance LO.LogicalConnective.PropLogicSymbols : LO.LogicalConnective Prop

Equations

• LO.LogicalConnective.PropLogicSymbols = LO.LogicalConnective.mk

@[simp]

theorem LO.LogicalConnective.Prop.top_eq : ⊤ = True

@[simp]

theorem LO.LogicalConnective.Prop.bot_eq : ⊥ = False

@[simp]

theorem LO.LogicalConnective.Prop.neg_eq (p : Prop) : ∼p = ¬p

@[simp]

theorem LO.LogicalConnective.Prop.arrow_eq (p : Prop) (q : Prop) : p ➝ q = (p → q)

@[simp]

theorem LO.LogicalConnective.Prop.and_eq (p : Prop) (q : Prop) : p ⋏ q = (p ∧ q)

@[simp]

theorem LO.LogicalConnective.Prop.or_eq (p : Prop) (q : Prop) : p ⋎ q = (p ∨ q)

@[simp]

theorem LO.LogicalConnective.Prop.iff_eq (p : Prop) (q : Prop) : p ⭤ q = (p ↔ q)

instance LO.LogicalConnective.instDeMorganProp : LO.DeMorgan Prop

Equations

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

class LO.LogicalConnective.HomClass (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [LO.LogicalConnective α] [LO.LogicalConnective β] [FunLike F α β] : Type

• map_top : ∀ (f : F), f ⊤ = ⊤
• map_bot : ∀ (f : F), f ⊥ = ⊥
• map_neg : ∀ (f : F) (p : α), f (∼p) = ∼f p
• map_imply : ∀ (f : F) (p q : α), f (p ➝ q) = f p ➝ f q
• map_and : ∀ (f : F) (p q : α), f (p ⋏ q) = f p ⋏ f q
• map_or : ∀ (f : F) (p q : α), f (p ⋎ q) = f p ⋎ f q

@[simp]

theorem LO.LogicalConnective.HomClass.map_top {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} [LO.LogicalConnective α] [LO.LogicalConnective β] [FunLike F α β] [self : LO.LogicalConnective.HomClass F α β] (f : F) : f ⊤ = ⊤

@[simp]

theorem LO.LogicalConnective.HomClass.map_bot {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} [LO.LogicalConnective α] [LO.LogicalConnective β] [FunLike F α β] [self : LO.LogicalConnective.HomClass F α β] (f : F) : f ⊥ = ⊥

@[simp]

theorem LO.LogicalConnective.HomClass.map_neg {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} [LO.LogicalConnective α] [LO.LogicalConnective β] [FunLike F α β] [self : LO.LogicalConnective.HomClass F α β] (f : F) (p : α) : f (∼p) = ∼f p

@[simp]

theorem LO.LogicalConnective.HomClass.map_imply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} [LO.LogicalConnective α] [LO.LogicalConnective β] [FunLike F α β] [self : LO.LogicalConnective.HomClass F α β] (f : F) (p : α) (q : α) : f (p ➝ q) = f p ➝ f q

@[simp]

theorem LO.LogicalConnective.HomClass.map_and {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} [LO.LogicalConnective α] [LO.LogicalConnective β] [FunLike F α β] [self : LO.LogicalConnective.HomClass F α β] (f : F) (p : α) (q : α) : f (p ⋏ q) = f p ⋏ f q

@[simp]

theorem LO.LogicalConnective.HomClass.map_or {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} [LO.LogicalConnective α] [LO.LogicalConnective β] [FunLike F α β] [self : LO.LogicalConnective.HomClass F α β] (f : F) (p : α) (q : α) : f (p ⋎ q) = f p ⋎ f q

instance LO.LogicalConnective.HomClass.instCoeFunForall (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [FunLike F α β] : CoeFun F fun (x : F) => α → β

Equations

• LO.LogicalConnective.HomClass.instCoeFunForall F α β = { coe := DFunLike.coe }

@[simp]

theorem LO.LogicalConnective.HomClass.map_iff (F : Type u_1) (α : outParam (Type u_2)) (β : outParam (Type u_3)) [LO.LogicalConnective α] [LO.LogicalConnective β] [FunLike F α β] [LO.LogicalConnective.HomClass F α β] (f : F) (a : α) (b : α) : f (a ⭤ b) = f a ⭤ f b

structure LO.LogicalConnective.Hom (α : Type u_1) (β : Type u_2) [LO.LogicalConnective α] [LO.LogicalConnective β] : Type (max u_1 u_2)

• toTr : α → β
• map_top' : self.toTr ⊤ = ⊤
• map_bot' : self.toTr ⊥ = ⊥
• map_neg' : ∀ (p : α), self.toTr (∼p) = ∼self.toTr p
• map_imply' : ∀ (p q : α), self.toTr (p ➝ q) = self.toTr p ➝ self.toTr q
• map_and' : ∀ (p q : α), self.toTr (p ⋏ q) = self.toTr p ⋏ self.toTr q
• map_or' : ∀ (p q : α), self.toTr (p ⋎ q) = self.toTr p ⋎ self.toTr q

theorem LO.LogicalConnective.Hom.map_top' {α : Type u_1} {β : Type u_2} [LO.LogicalConnective α] [LO.LogicalConnective β] (self : α →ˡᶜ β) : self.toTr ⊤ = ⊤

theorem LO.LogicalConnective.Hom.map_bot' {α : Type u_1} {β : Type u_2} [LO.LogicalConnective α] [LO.LogicalConnective β] (self : α →ˡᶜ β) : self.toTr ⊥ = ⊥

theorem LO.LogicalConnective.Hom.map_neg' {α : Type u_1} {β : Type u_2} [LO.LogicalConnective α] [LO.LogicalConnective β] (self : α →ˡᶜ β) (p : α) : self.toTr (∼p) = ∼self.toTr p

theorem LO.LogicalConnective.Hom.map_imply' {α : Type u_1} {β : Type u_2} [LO.LogicalConnective α] [LO.LogicalConnective β] (self : α →ˡᶜ β) (p : α) (q : α) : self.toTr (p ➝ q) = self.toTr p ➝ self.toTr q

theorem LO.LogicalConnective.Hom.map_and' {α : Type u_1} {β : Type u_2} [LO.LogicalConnective α] [LO.LogicalConnective β] (self : α →ˡᶜ β) (p : α) (q : α) : self.toTr (p ⋏ q) = self.toTr p ⋏ self.toTr q

theorem LO.LogicalConnective.Hom.map_or' {α : Type u_1} {β : Type u_2} [LO.LogicalConnective α] [LO.LogicalConnective β] (self : α →ˡᶜ β) (p : α) (q : α) : self.toTr (p ⋎ q) = self.toTr p ⋎ self.toTr q

def LO.LogicalConnective.«term_→ˡᶜ_» : Lean.TrailingParserDescr

Equations

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

instance LO.LogicalConnective.Hom.instFunLike {α : Type u_1} {β : Type u_2} [LO.LogicalConnective α] [LO.LogicalConnective β] : FunLike (α →ˡᶜ β) α β

Equations

• LO.LogicalConnective.Hom.instFunLike = { coe := LO.LogicalConnective.Hom.toTr, coe_injective' := ⋯ }

instance LO.LogicalConnective.Hom.instCoeFunForall {α : Type u_1} {β : Type u_2} [LO.LogicalConnective α] [LO.LogicalConnective β] : CoeFun (α →ˡᶜ β) fun (x : α →ˡᶜ β) => α → β

Equations

• LO.LogicalConnective.Hom.instCoeFunForall = DFunLike.hasCoeToFun

theorem LO.LogicalConnective.Hom.ext {α : Type u_1} {β : Type u_2} [LO.LogicalConnective α] [LO.LogicalConnective β] (f : α →ˡᶜ β) (g : α →ˡᶜ β) (h : ∀ (x : α), f x = g x) : f = g

instance LO.LogicalConnective.Hom.instHomClass {α : Type u_1} {β : Type u_2} [LO.LogicalConnective α] [LO.LogicalConnective β] : LO.LogicalConnective.HomClass (α →ˡᶜ β) α β

Equations

• LO.LogicalConnective.Hom.instHomClass = { map_top := ⋯, map_bot := ⋯, map_neg := ⋯, map_imply := ⋯, map_and := ⋯, map_or := ⋯ }

def LO.LogicalConnective.Hom.id {α : Type u_1} [LO.LogicalConnective α] : α →ˡᶜ α

Equations

• LO.LogicalConnective.Hom.id = { toTr := id, map_top' := ⋯, map_bot' := ⋯, map_neg' := ⋯, map_imply' := ⋯, map_and' := ⋯, map_or' := ⋯ }

@[simp]

theorem LO.LogicalConnective.Hom.app_id {α : Type u_1} [LO.LogicalConnective α] (a : α) : LO.LogicalConnective.Hom.id a = a

def LO.LogicalConnective.Hom.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LO.LogicalConnective α] [LO.LogicalConnective β] [LO.LogicalConnective γ] (g : β →ˡᶜ γ) (f : α →ˡᶜ β) : α →ˡᶜ γ

Equations

• g.comp f = { toTr := ⇑g ∘ ⇑f, map_top' := ⋯, map_bot' := ⋯, map_neg' := ⋯, map_imply' := ⋯, map_and' := ⋯, map_or' := ⋯ }

@[simp]

theorem LO.LogicalConnective.Hom.app_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LO.LogicalConnective α] [LO.LogicalConnective β] [LO.LogicalConnective γ] (g : β →ˡᶜ γ) (f : α →ˡᶜ β) (a : α) : (g.comp f) a = g (f a)

def LO.LogicalConnective.ball {α : ℕ → Type u_4} [(i : ℕ) → LO.LogicalConnective (α i)] [LO.UnivQuantifier α] {n : ℕ} (p : α (n + 1)) (q : α (n + 1)) : α n

Equations

• (∀[p] q) = ∀' (p ➝ q)

def LO.LogicalConnective.bex {α : ℕ → Type u_4} [(i : ℕ) → LO.LogicalConnective (α i)] [LO.ExQuantifier α] {n : ℕ} (p : α (n + 1)) (q : α (n + 1)) : α n

Equations

• (∃[p] q) = ∃' p ⋏ q

def LO.LogicalConnective.«term∀[_]_» : Lean.ParserDescr

Equations

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

def LO.LogicalConnective.«term∃[_]_» : Lean.ParserDescr

Equations

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

class LO.LogicalConnective.AndOrClosed {F : Type u_4} [LO.LogicalConnective F] (C : F → Prop) : Type

• verum : C ⊤
• falsum : C ⊥
• and : ∀ {f g : F}, C f → C g → C (f ⋏ g)
• or : ∀ {f g : F}, C f → C g → C (f ⋎ g)

@[simp]

theorem LO.LogicalConnective.AndOrClosed.verum {F : Type u_4} [LO.LogicalConnective F] {C : F → Prop} [self : LO.LogicalConnective.AndOrClosed C] : C ⊤

@[simp]

theorem LO.LogicalConnective.AndOrClosed.falsum {F : Type u_4} [LO.LogicalConnective F] {C : F → Prop} [self : LO.LogicalConnective.AndOrClosed C] : C ⊥

theorem LO.LogicalConnective.AndOrClosed.and {F : Type u_4} [LO.LogicalConnective F] {C : F → Prop} [self : LO.LogicalConnective.AndOrClosed C] {f : F} {g : F} : C f → C g → C (f ⋏ g)

theorem LO.LogicalConnective.AndOrClosed.or {F : Type u_4} [LO.LogicalConnective F] {C : F → Prop} [self : LO.LogicalConnective.AndOrClosed C] {f : F} {g : F} : C f → C g → C (f ⋎ g)

class LO.LogicalConnective.Closed {F : Type u_4} [LO.LogicalConnective F] (C : F → Prop) extends LO.LogicalConnective.AndOrClosed : Type

• verum : C ⊤
• falsum : C ⊥
• and : ∀ {f g : F}, C f → C g → C (f ⋏ g)
• or : ∀ {f g : F}, C f → C g → C (f ⋎ g)
• not : ∀ {f : F}, C f → C (∼f)
• imply : ∀ {f g : F}, C f → C g → C (f ➝ g)

theorem LO.LogicalConnective.Closed.not {F : Type u_4} [LO.LogicalConnective F] {C : F → Prop} [self : LO.LogicalConnective.Closed C] {f : F} : C f → C (∼f)

theorem LO.LogicalConnective.Closed.imply {F : Type u_4} [LO.LogicalConnective F] {C : F → Prop} [self : LO.LogicalConnective.Closed C] {f : F} {g : F} : C f → C g → C (f ➝ g)

class LO.Tilde.Subclosed {F : Type u_1} [LO.Tilde F] (C : F → Prop) : Type

• tilde_closed : ∀ {p : F}, C (∼p) → C p

theorem LO.Tilde.Subclosed.tilde_closed {F : Type u_1} [LO.Tilde F] {C : F → Prop} [self : LO.Tilde.Subclosed C] {p : F} : C (∼p) → C p

class LO.Arrow.Subclosed {F : Type u_1} [LO.Arrow F] (C : F → Prop) : Type

• arrow_closed : ∀ {p q : F}, C (p ➝ q) → C p ∧ C q

theorem LO.Arrow.Subclosed.arrow_closed {F : Type u_1} [LO.Arrow F] {C : F → Prop} [self : LO.Arrow.Subclosed C] {p : F} {q : F} : C (p ➝ q) → C p ∧ C q

class LO.Wedge.Subclosed {F : Type u_1} [LO.Wedge F] (C : F → Prop) : Type

• wedge_closed : ∀ {p q : F}, C (p ⋏ q) → C p ∧ C q

theorem LO.Wedge.Subclosed.wedge_closed {F : Type u_1} [LO.Wedge F] {C : F → Prop} [self : LO.Wedge.Subclosed C] {p : F} {q : F} : C (p ⋏ q) → C p ∧ C q

class LO.Vee.Subclosed {F : Type u_1} [LO.Vee F] (C : F → Prop) : Type

• vee_closed : ∀ {p q : F}, C (p ⋎ q) → C p ∧ C q

theorem LO.Vee.Subclosed.vee_closed {F : Type u_1} [LO.Vee F] {C : F → Prop} [self : LO.Vee.Subclosed C] {p : F} {q : F} : C (p ⋎ q) → C p ∧ C q

class LO.LogicalConnective.Subclosed {F : Type u_1} [LO.LogicalConnective F] (C : F → Prop) extends LO.Tilde.Subclosed , LO.Arrow.Subclosed , LO.Wedge.Subclosed , LO.Vee.Subclosed : Type

def LO.conjLt {α : Type u_1} [LO.LogicalConnective α] (p : ℕ → α) : ℕ → α

Equations

• LO.conjLt p 0 = ⊤
• LO.conjLt p k.succ = p k ⋏ LO.conjLt p k

@[simp]

theorem LO.conjLt_zero {α : Type u_1} [LO.LogicalConnective α] (p : ℕ → α) : LO.conjLt p 0 = ⊤

@[simp]

theorem LO.conjLt_succ {α : Type u_1} [LO.LogicalConnective α] (p : ℕ → α) (k : ℕ) : LO.conjLt p (k + 1) = p k ⋏ LO.conjLt p k

@[simp]

theorem LO.hom_conj_prop {α : Type u_1} [LO.LogicalConnective α] {F : Type u_3} {k : ℕ} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (p : ℕ → α) : f (LO.conjLt p k) ↔ ∀ i < k, f (p i)

def LO.disjLt {α : Type u_1} [LO.LogicalConnective α] (p : ℕ → α) : ℕ → α

Equations

• LO.disjLt p 0 = ⊥
• LO.disjLt p k.succ = p k ⋎ LO.disjLt p k

@[simp]

theorem LO.disjLt_zero {α : Type u_1} [LO.LogicalConnective α] (p : ℕ → α) : LO.disjLt p 0 = ⊥

@[simp]

theorem LO.disjLt_succ {α : Type u_1} [LO.LogicalConnective α] (p : ℕ → α) (k : ℕ) : LO.disjLt p (k + 1) = p k ⋎ LO.disjLt p k

@[simp]

theorem LO.hom_disj_prop {α : Type u_1} [LO.LogicalConnective α] {F : Type u_3} {k : ℕ} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (p : ℕ → α) : f (LO.disjLt p k) ↔ ∃ i < k, f (p i)

def Matrix.conj {α : Type u_1} [LO.LogicalConnective α] {n : ℕ} : (Fin n → α) → α

Equations

• Matrix.conj x_2 = ⊤
• Matrix.conj v = v 0 ⋏ Matrix.conj (Matrix.vecTail v)

@[simp]

theorem Matrix.conj_nil {α : Type u_1} [LO.LogicalConnective α] (v : Fin 0 → α) : Matrix.conj v = ⊤

@[simp]

theorem Matrix.conj_cons {α : Type u_1} [LO.LogicalConnective α] {n : ℕ} {a : α} {v : Fin n → α} : Matrix.conj (a :> v) = a ⋏ Matrix.conj v

@[simp]

theorem Matrix.conj_hom_prop {α : Type u_1} [LO.LogicalConnective α] {F : Type u_2} {n : ℕ} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (v : Fin n → α) : f (Matrix.conj v) = ∀ (i : Fin n), f (v i)

theorem Matrix.hom_conj {β : Type u_3} {α : Type u_1} [LO.LogicalConnective α] [LO.LogicalConnective β] {F : Type u_2} {n : ℕ} [FunLike F α β] [LO.LogicalConnective.HomClass F α β] (f : F) (v : Fin n → α) : f (Matrix.conj v) = Matrix.conj (⇑f ∘ v)

theorem Matrix.hom_conj₂ {β : Type u_3} {α : Type u_1} [LO.LogicalConnective α] [LO.LogicalConnective β] {F : Type u_2} {n : ℕ} [FunLike F α β] [LO.LogicalConnective.HomClass F α β] (f : F) (v : Fin n → α) : f (Matrix.conj v) = Matrix.conj fun (i : Fin n) => f (v i)

def Matrix.disj {α : Type u_1} [LO.LogicalConnective α] {n : ℕ} : (Fin n → α) → α

Equations

• Matrix.disj x_2 = ⊥
• Matrix.disj v = v 0 ⋎ Matrix.disj (Matrix.vecTail v)

@[simp]

theorem Matrix.disj_nil {α : Type u_1} [LO.LogicalConnective α] (v : Fin 0 → α) : Matrix.disj v = ⊥

@[simp]

theorem Matrix.disj_cons {α : Type u_1} [LO.LogicalConnective α] {n : ℕ} {a : α} {v : Fin n → α} : Matrix.disj (a :> v) = a ⋎ Matrix.disj v

@[simp]

theorem Matrix.disj_hom_prop {α : Type u_1} [LO.LogicalConnective α] {F : Type u_2} {n : ℕ} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (v : Fin n → α) : f (Matrix.disj v) = ∃ (i : Fin n), f (v i)

theorem Matrix.hom_disj {β : Type u_3} {α : Type u_1} [LO.LogicalConnective α] [LO.LogicalConnective β] {F : Type u_2} {n : ℕ} [FunLike F α β] [LO.LogicalConnective.HomClass F α β] (f : F) (v : Fin n → α) : f (Matrix.disj v) = Matrix.disj (⇑f ∘ v)

theorem Matrix.hom_disj' {β : Type u_3} {α : Type u_1} [LO.LogicalConnective α] [LO.LogicalConnective β] {F : Type u_2} {n : ℕ} [FunLike F α β] [LO.LogicalConnective.HomClass F α β] (f : F) (v : Fin n → α) : f (Matrix.disj v) = Matrix.disj fun (i : Fin n) => f (v i)

def List.conj {α : Type u_1} [LO.LogicalConnective α] : List α → α

Equations

• [].conj = ⊤
• (a :: as).conj = a ⋏ as.conj

@[simp]

theorem List.conj_nil {α : Type u_1} [LO.LogicalConnective α] : [].conj = ⊤

@[simp]

theorem List.conj_cons {α : Type u_1} [LO.LogicalConnective α] {a : α} {as : List α} : (a :: as).conj = a ⋏ as.conj

theorem List.map_conj {α : Type u_1} [LO.LogicalConnective α] {F : Type u_2} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (l : List α) : f l.conj ↔ ∀ a ∈ l, f a

theorem List.map_conj_append {α : Type u_1} [LO.LogicalConnective α] {F : Type u_2} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (l₁ : List α) (l₂ : List α) : f (l₁ ++ l₂).conj ↔ f (l₁.conj ⋏ l₂.conj)

def List.disj {α : Type u_1} [LO.LogicalConnective α] : List α → α

Equations

• [].disj = ⊥
• (a :: as).disj = a ⋎ as.disj

@[simp]

theorem List.disj_nil {α : Type u_1} [LO.LogicalConnective α] : [].disj = ⊥

@[simp]

theorem List.disj_cons {α : Type u_1} [LO.LogicalConnective α] {a : α} {as : List α} : (a :: as).disj = a ⋎ as.disj

theorem List.map_disj {α : Type u_1} [LO.LogicalConnective α] {F : Type u_2} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (l : List α) : f l.disj ↔ ∃ a ∈ l, f a

theorem List.map_disj_append {α : Type u_1} [LO.LogicalConnective α] {F : Type u_2} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (l₁ : List α) (l₂ : List α) : f (l₁ ++ l₂).disj ↔ f (l₁.disj ⋎ l₂.disj)

def List.conj₂ {F : Type u} [LO.LogicalConnective F] : List F → F

Remark: [p].conj₂ = p ≠ p ⋏ ⊤ = [p].conj

Equations

• ⋀[] = ⊤
• ⋀[p] = p
• ⋀(p :: q :: rs) = p ⋏ ⋀(q :: rs)

def List.«term⋀_» : Lean.ParserDescr

Equations

• List.«term⋀_» = Lean.ParserDescr.node `List.term⋀_ 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋀") (Lean.ParserDescr.cat `term 80))

@[simp]

theorem List.conj₂_nil {F : Type u} [LO.LogicalConnective F] : ⋀[] = ⊤

@[simp]

theorem List.conj₂_singleton {F : Type u} [LO.LogicalConnective F] {p : F} : ⋀[p] = p

@[simp]

theorem List.conj₂_doubleton {F : Type u} [LO.LogicalConnective F] {p : F} {q : F} : ⋀[p, q] = p ⋏ q

@[simp]

theorem List.conj₂_cons_nonempty {F : Type u} [LO.LogicalConnective F] {a : F} {as : List F} (h : autoParam (as ≠ []) _auto✝) : ⋀(a :: as) = a ⋏ ⋀as

def List.disj₂ {F : Type u} [LO.LogicalConnective F] : List F → F

Remark: [p].disj = p ≠ p ⋎ ⊥ = [p].disj

Equations

• ⋁[] = ⊥
• ⋁[p] = p
• ⋁(p :: q :: rs) = p ⋎ ⋁(q :: rs)

def List.«term⋁_» : Lean.ParserDescr

Equations

• List.«term⋁_» = Lean.ParserDescr.node `List.term⋁_ 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⋁") (Lean.ParserDescr.cat `term 80))

@[simp]

theorem List.disj₂_nil {F : Type u} [LO.LogicalConnective F] : ⋁[] = ⊥

@[simp]

theorem List.disj₂_singleton {F : Type u} [LO.LogicalConnective F] {p : F} : ⋁[p] = p

@[simp]

theorem List.disj₂_doubleton {F : Type u} [LO.LogicalConnective F] {p : F} {q : F} : ⋁[p, q] = p ⋎ q

@[simp]

theorem List.disj₂_cons_nonempty {F : Type u} [LO.LogicalConnective F] {a : F} {as : List F} (h : autoParam (as ≠ []) _auto✝) : ⋁(a :: as) = a ⋎ ⋁as

theorem List.induction_with_singleton {F : Type u} {motive : List F → Prop} (hnil : motive []) (hsingle : ∀ (a : F), motive [a]) (hcons : ∀ (a : F) (as : List F), as ≠ [] → motive as → motive (a :: as)) (as : List F) : motive as

noncomputable def Finset.conj {α : Type u_1} [LO.LogicalConnective α] (s : Finset α) : α

Equations

• s.conj = s.toList.conj

theorem Finset.map_conj {α : Type u_2} [LO.LogicalConnective α] {F : Type u_1} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (s : Finset α) : f s.conj ↔ ∀ a ∈ s, f a

theorem Finset.map_conj_union {α : Type u_2} [LO.LogicalConnective α] [DecidableEq α] {F : Type u_1} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (s₁ : Finset α) (s₂ : Finset α) : f (s₁ ∪ s₂).conj ↔ f (s₁.conj ⋏ s₂.conj)

noncomputable def Finset.disj {α : Type u_1} [LO.LogicalConnective α] (s : Finset α) : α

Equations

• s.disj = s.toList.disj

theorem Finset.map_disj {α : Type u_2} [LO.LogicalConnective α] {F : Type u_1} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (s : Finset α) : f s.disj ↔ ∃ a ∈ s, f a

theorem Finset.map_disj_union {α : Type u_2} [LO.LogicalConnective α] [DecidableEq α] {F : Type u_1} [FunLike F α Prop] [LO.LogicalConnective.HomClass F α Prop] (f : F) (s₁ : Finset α) (s₂ : Finset α) : f (s₁ ∪ s₂).disj ↔ f (s₁.disj ⋎ s₂.disj)