Documentation
Foundation
.
Modal
.
Hilbert
.
WeakerThan
.
KTB_S5
Search
Google site search
return to top
source
Imports
Init
Foundation.Modal.Kripke.Geach.Systems
Imported by
LO
.
Modal
.
Hilbert
.
KTB_weakerThan_S5
LO
.
Modal
.
Hilbert
.
KTB_strictlyWeakerThan_S5
source
theorem
LO
.
Modal
.
Hilbert
.
KTB_weakerThan_S5
:
LO.Modal.Hilbert.KTB
ℕ
≤ₛ
LO.Modal.Hilbert.S5
ℕ
source
theorem
LO
.
Modal
.
Hilbert
.
KTB_strictlyWeakerThan_S5
:
LO.Modal.Hilbert.KTB
ℕ
<ₛ
LO.Modal.Hilbert.S5
ℕ