Documentation
Foundation
.
Modal
.
Hilbert
.
WeakerThan
.
S4_S5
Search
Google site search
return to top
source
Imports
Init
Foundation.Modal.Kripke.Geach.Systems
Imported by
LO
.
Modal
.
Hilbert
.
S4_weakerThan_S5
LO
.
Modal
.
Hilbert
.
S4_strictlyWeakerThan_S5
source
theorem
LO
.
Modal
.
Hilbert
.
S4_weakerThan_S5
:
LO.Modal.Hilbert.S4
ℕ
≤ₛ
LO.Modal.Hilbert.S5
ℕ
source
theorem
LO
.
Modal
.
Hilbert
.
S4_strictlyWeakerThan_S5
:
LO.Modal.Hilbert.S4
ℕ
<ₛ
LO.Modal.Hilbert.S5
ℕ