@[reducible, inline]
◇
is duality of □
.
@[reducible, inline]
Equations
- LO.Axioms.DiaDuality.set = {x : F | ∃ (φ : F), LO.Axioms.DiaDuality φ = x}
@[reducible, inline]
Equations
- LO.Axioms.«term𝗞» = Lean.ParserDescr.node `LO.Axioms.«term𝗞» 1024 (Lean.ParserDescr.symbol "𝗞")
@[reducible, inline]
Equations
- LO.Axioms.T φ = □φ ➝ φ
@[reducible, inline]
Equations
- 𝗧 = {x : F | ∃ (φ : F), LO.Axioms.T φ = x}
Equations
- LO.Axioms.«term𝗧» = Lean.ParserDescr.node `LO.Axioms.«term𝗧» 1024 (Lean.ParserDescr.symbol "𝗧")
@[reducible, inline]
Equations
- LO.Axioms.B φ = φ ➝ □◇φ
@[reducible, inline]
Equations
- 𝗕 = {x : F | ∃ (φ : F), LO.Axioms.B φ = x}
Equations
- LO.Axioms.«term𝗕» = Lean.ParserDescr.node `LO.Axioms.«term𝗕» 1024 (Lean.ParserDescr.symbol "𝗕")
@[reducible, inline]
□
-only version of axiom 𝗕
.
@[reducible, inline]
Equations
- 𝗕(□) = {x : F | ∃ (φ : F), LO.Axioms.B₂ φ = x}
Equations
- LO.Axioms.«term𝗕(□)» = Lean.ParserDescr.node `LO.Axioms.«term𝗕(□)» 1024 (Lean.ParserDescr.symbol "𝗕(□)")
@[reducible, inline]
Equations
- LO.Axioms.D φ = □φ ➝ ◇φ
@[reducible, inline]
Equations
- 𝗗 = {x : F | ∃ (φ : F), LO.Axioms.D φ = x}
Equations
- LO.Axioms.«term𝗗» = Lean.ParserDescr.node `LO.Axioms.«term𝗗» 1024 (Lean.ParserDescr.symbol "𝗗")
@[reducible, inline]
Equations
@[reducible, inline]
Equations
- 𝗣 = {x : F | LO.Axioms.P = x}
Equations
- LO.Axioms.«term𝗣» = Lean.ParserDescr.node `LO.Axioms.«term𝗣» 1024 (Lean.ParserDescr.symbol "𝗣")
@[reducible, inline]
@[reducible, inline]
Equations
- 𝟰 = {x : F | ∃ (φ : F), LO.Axioms.Four φ = x}
Equations
- LO.Axioms.«term𝟰» = Lean.ParserDescr.node `LO.Axioms.«term𝟰» 1024 (Lean.ParserDescr.symbol "𝟰")
@[reducible, inline]
@[reducible, inline]
Equations
- 𝟱 = {x : F | ∃ (φ : F), LO.Axioms.Five φ = x}
Equations
- LO.Axioms.«term𝟱» = Lean.ParserDescr.node `LO.Axioms.«term𝟱» 1024 (Lean.ParserDescr.symbol "𝟱")
@[reducible, inline]
□
-only version of axiom 𝟱
.
@[reducible, inline]
Equations
- 𝟱(□) = {x : F | ∃ (φ : F), LO.Axioms.Five₂ φ = x}
Equations
- LO.Axioms.«term𝟱(□)» = Lean.ParserDescr.node `LO.Axioms.«term𝟱(□)» 1024 (Lean.ParserDescr.symbol "𝟱(□)")
@[reducible, inline]
@[reducible, inline]
Equations
- .𝟮 = {x : F | ∃ (φ : F), LO.Axioms.Dot2 φ = x}
Equations
- LO.Axioms.«term.𝟮» = Lean.ParserDescr.node `LO.Axioms.«term.𝟮» 1024 (Lean.ParserDescr.symbol ".𝟮")
@[reducible, inline]
@[reducible, inline]
Equations
- 𝗖𝟰 = {x : F | ∃ (φ : F), LO.Axioms.C4 φ = x}
Equations
- LO.Axioms.«term𝗖𝟰» = Lean.ParserDescr.node `LO.Axioms.«term𝗖𝟰» 1024 (Lean.ParserDescr.symbol "𝗖𝟰")
@[reducible, inline]
Equations
- LO.Axioms.CD φ = ◇φ ➝ □φ
@[reducible, inline]
Equations
- 𝗖𝗗 = {x : F | ∃ (φ : F), LO.Axioms.CD φ = x}
Equations
- LO.Axioms.«term𝗖𝗗» = Lean.ParserDescr.node `LO.Axioms.«term𝗖𝗗» 1024 (Lean.ParserDescr.symbol "𝗖𝗗")
@[reducible, inline]
Equations
- LO.Axioms.Tc φ = φ ➝ □φ
@[reducible, inline]
Equations
- 𝗧𝗰 = {x : F | ∃ (φ : F), LO.Axioms.Tc φ = x}
Equations
- LO.Axioms.«term𝗧𝗰» = Lean.ParserDescr.node `LO.Axioms.«term𝗧𝗰» 1024 (Lean.ParserDescr.symbol "𝗧𝗰")
@[reducible, inline]
Equations
- LO.Axioms.Ver φ = □φ
@[reducible, inline]
Equations
- 𝗩𝗲𝗿 = {x : F | ∃ (φ : F), LO.Axioms.Ver φ = x}
Equations
- LO.Axioms.«term𝗩𝗲𝗿» = Lean.ParserDescr.node `LO.Axioms.«term𝗩𝗲𝗿» 1024 (Lean.ParserDescr.symbol "𝗩𝗲𝗿")
@[reducible, inline]
@[reducible, inline]
Equations
- .𝟯 = {x : F | ∃ (φ : F) (ψ : F), LO.Axioms.Dot3 φ ψ = x}
Equations
- LO.Axioms.«term.𝟯» = Lean.ParserDescr.node `LO.Axioms.«term.𝟯» 1024 (Lean.ParserDescr.symbol ".𝟯")
@[reducible, inline]
Equations
- LO.Axioms.«term𝗚𝗿𝘇» = Lean.ParserDescr.node `LO.Axioms.«term𝗚𝗿𝘇» 1024 (Lean.ParserDescr.symbol "𝗚𝗿𝘇")
@[reducible, inline]
@[reducible, inline]
Equations
- 𝗠 = {x : F | ∃ (φ : F), LO.Axioms.M φ = x}
Equations
- LO.Axioms.«term𝗠» = Lean.ParserDescr.node `LO.Axioms.«term𝗠» 1024 (Lean.ParserDescr.symbol "𝗠")
@[reducible, inline]
Equations
- LO.Axioms.«term𝗟» = Lean.ParserDescr.node `LO.Axioms.«term𝗟» 1024 (Lean.ParserDescr.symbol "𝗟")
@[reducible, inline]
Equations
- LO.Axioms.«term𝗛» = Lean.ParserDescr.node `LO.Axioms.«term𝗛» 1024 (Lean.ParserDescr.symbol "𝗛")
@[reducible, inline]
abbrev
LO.Axioms.Geach
{F : Type u_1}
[BasicModalLogicalConnective F]
(t : GeachConfluent.Taple)
(φ : F)
:
F
@[reducible, inline]
abbrev
LO.Axioms.Geach.set
{F : Type u_1}
[BasicModalLogicalConnective F]
(t : GeachConfluent.Taple)
:
Set F
Equations
- 𝗴𝗲(t) = {x : F | ∃ (φ : F), LO.Axioms.Geach t φ = x}
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
LO.Axioms.MultiGeach.def_one
{F : Type u_1}
[BasicModalLogicalConnective F]
{t : GeachConfluent.Taple}
:
theorem
LO.Axioms.MultiGeach.def_two
{F : Type u_1}
[BasicModalLogicalConnective F]
{t₁ t₂ : GeachConfluent.Taple}
:
@[simp]
theorem
LO.Axioms.MultiGeach.iff_cons
{F : Type u_1}
[BasicModalLogicalConnective F]
{x : GeachConfluent.Taple}
{l : List GeachConfluent.Taple}
:
theorem
LO.Axioms.MultiGeach.mem
{F : Type u_1}
[BasicModalLogicalConnective F]
{l : List GeachConfluent.Taple}
{x : GeachConfluent.Taple}
(h : x ∈ l)
: