Documentation
Foundation
.
Modal
.
Hilbert
.
WeakerThan
.
KDB_KTB
Search
Google site search
return to top
source
Imports
Init
Foundation.Modal.Kripke.Geach.Systems
Imported by
LO
.
Modal
.
Hilbert
.
KDB_weakerThan_KTB
LO
.
Modal
.
Hilbert
.
KDB_strictlyWeakerThan_KTB
source
theorem
LO
.
Modal
.
Hilbert
.
KDB_weakerThan_KTB
:
LO.Modal.Hilbert.KDB
ℕ
≤ₛ
LO.Modal.Hilbert.KTB
ℕ
source
theorem
LO
.
Modal
.
Hilbert
.
KDB_strictlyWeakerThan_KTB
:
LO.Modal.Hilbert.KDB
ℕ
<ₛ
LO.Modal.Hilbert.KTB
ℕ