Documentation
Foundation
.
Modal
.
Hilbert
.
WeakerThan
.
K45_KB4
Search
Google site search
return to top
source
Imports
Init
Foundation.Modal.Kripke.Geach.Systems
Imported by
LO
.
Modal
.
Hilbert
.
K45_weakerThan_KB4
LO
.
Modal
.
Hilbert
.
K45_strictlyWeakerThan_KB4
source
theorem
LO
.
Modal
.
Hilbert
.
K45_weakerThan_KB4
:
LO.Modal.Hilbert.K45
ℕ
≤ₛ
LO.Modal.Hilbert.KB4
ℕ
source
theorem
LO
.
Modal
.
Hilbert
.
K45_strictlyWeakerThan_KB4
:
LO.Modal.Hilbert.K45
ℕ
<ₛ
LO.Modal.Hilbert.KB4
ℕ