@[reducible, inline]
abbrev
LO.Axioms.DiaDuality
{F : Type u_1}
[LO.LogicalConnective F]
[LO.Box F]
(p : F)
[LO.Dia F]
:
F
◇
is duality of □
.
Instances For
@[reducible, inline]
abbrev
LO.Axioms.DiaDuality.set
{F : Type u_1}
[LO.LogicalConnective F]
[LO.Box F]
[LO.Dia F]
:
Set F
Equations
- LO.Axioms.DiaDuality.set = {x : F | ∃ (p : F), LO.Axioms.DiaDuality p = x}
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Axioms.«term𝗞» = Lean.ParserDescr.node `LO.Axioms.term𝗞 1024 (Lean.ParserDescr.symbol "𝗞")
Instances For
Equations
- LO.Axioms.«term𝗧» = Lean.ParserDescr.node `LO.Axioms.term𝗧 1024 (Lean.ParserDescr.symbol "𝗧")
Instances For
Equations
- LO.Axioms.«term𝗕» = Lean.ParserDescr.node `LO.Axioms.term𝗕 1024 (Lean.ParserDescr.symbol "𝗕")
Instances For
@[reducible, inline]
□
-only version of axiom 𝗕
.
Instances For
Equations
- LO.Axioms.«term𝗕(□)» = Lean.ParserDescr.node `LO.Axioms.term𝗕(□) 1024 (Lean.ParserDescr.symbol "𝗕(□)")
Instances For
Equations
- LO.Axioms.«term𝗗» = Lean.ParserDescr.node `LO.Axioms.term𝗗 1024 (Lean.ParserDescr.symbol "𝗗")
Instances For
@[reducible, inline]
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Axioms.«term𝗣» = Lean.ParserDescr.node `LO.Axioms.term𝗣 1024 (Lean.ParserDescr.symbol "𝗣")
Instances For
@[simp]
@[reducible, inline]
Instances For
Equations
- LO.Axioms.«term𝟰» = Lean.ParserDescr.node `LO.Axioms.term𝟰 1024 (Lean.ParserDescr.symbol "𝟰")
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Axioms.«term𝟱» = Lean.ParserDescr.node `LO.Axioms.term𝟱 1024 (Lean.ParserDescr.symbol "𝟱")
Instances For
@[reducible, inline]
□
-only version of axiom 𝟱
.
Instances For
Equations
- LO.Axioms.«term𝟱(□)» = Lean.ParserDescr.node `LO.Axioms.term𝟱(□) 1024 (Lean.ParserDescr.symbol "𝟱(□)")
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Axioms.«term.𝟮» = Lean.ParserDescr.node `LO.Axioms.term.𝟮 1024 (Lean.ParserDescr.symbol ".𝟮")
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Axioms.«term𝗖𝟰» = Lean.ParserDescr.node `LO.Axioms.term𝗖𝟰 1024 (Lean.ParserDescr.symbol "𝗖𝟰")
Instances For
Equations
- LO.Axioms.«term𝗖𝗗» = Lean.ParserDescr.node `LO.Axioms.term𝗖𝗗 1024 (Lean.ParserDescr.symbol "𝗖𝗗")
Instances For
Equations
- LO.Axioms.«term𝗧𝗰» = Lean.ParserDescr.node `LO.Axioms.term𝗧𝗰 1024 (Lean.ParserDescr.symbol "𝗧𝗰")
Instances For
Equations
- LO.Axioms.«term𝗩𝗲𝗿» = Lean.ParserDescr.node `LO.Axioms.term𝗩𝗲𝗿 1024 (Lean.ParserDescr.symbol "𝗩𝗲𝗿")
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Axioms.«term.𝟯» = Lean.ParserDescr.node `LO.Axioms.term.𝟯 1024 (Lean.ParserDescr.symbol ".𝟯")
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Axioms.«term𝗚𝗿𝘇» = Lean.ParserDescr.node `LO.Axioms.term𝗚𝗿𝘇 1024 (Lean.ParserDescr.symbol "𝗚𝗿𝘇")
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Axioms.«term𝗠» = Lean.ParserDescr.node `LO.Axioms.term𝗠 1024 (Lean.ParserDescr.symbol "𝗠")
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Axioms.«term𝗟» = Lean.ParserDescr.node `LO.Axioms.term𝗟 1024 (Lean.ParserDescr.symbol "𝗟")
Instances For
@[reducible, inline]
Instances For
Equations
- LO.Axioms.«term𝗛» = Lean.ParserDescr.node `LO.Axioms.term𝗛 1024 (Lean.ParserDescr.symbol "𝗛")