Documentation
Foundation
.
Modal
.
Boxdot
.
Basic
Search
return to top
source
Imports
Init
Foundation.Modal.Hilbert.Basic
Imported by
LO
.
Modal
.
Formula
.
BoxdotTranslation
LO
.
Modal
.
«term_ᵇ»
LO
.
Modal
.
BoxdotProperty
LO
.
Modal
.
boxdotTranslated
source
def
LO
.
Modal
.
Formula
.
BoxdotTranslation
{α :
Type
u_1}
:
Formula
α
→
Formula
α
Equations
LO.Modal.Formula.atom
a
ᵇ
=
LO.Modal.Formula.atom
a
LO.Modal.Formula.falsum
ᵇ
=
⊥
φ
.imp
ψ
ᵇ
=
φ
ᵇ
➝
ψ
ᵇ
φ
.box
ᵇ
=
⊡
φ
ᵇ
Instances For
source
def
LO
.
Modal
.
«term_ᵇ»
:
Lean.TrailingParserDescr
Equations
LO.Modal.«term_ᵇ»
=
Lean.ParserDescr.trailingNode
`LO.Modal.«term_ᵇ»
90
90
(
Lean.ParserDescr.symbol
"ᵇ"
)
Instances For
source
class
LO
.
Modal
.
BoxdotProperty
{α :
Type
u_1}
(H₁ H₂ :
Hilbert
α
)
:
Prop
bdp
{φ :
Formula
α
}
:
H₁
⊢!
φ
ᵇ
↔
H₂
⊢!
φ
Instances
source
theorem
LO
.
Modal
.
boxdotTranslated
{α :
Type
u_1}
[
DecidableEq
α
]
{φ :
Formula
α
}
{H₁ H₂ :
Hilbert
α
}
[
H₁
.IsNormal
]
[
H₂
.IsNormal
]
(h :
∀
φ
∈
H₁
.axioms
,
H₂
⊢!
φ
ᵇ
)
:
H₁
⊢!
φ
→
H₂
⊢!
φ
ᵇ