Documentation
Foundation
.
Modal
.
Hilbert
.
WeakerThan
.
KD4_KD45
Search
Google site search
return to top
source
Imports
Init
Foundation.Modal.Kripke.Geach.Systems
Imported by
LO
.
Modal
.
Hilbert
.
KD4_weakerThan_KD45
LO
.
Modal
.
Hilbert
.
KD4_strictlyWeakerThan_KD45
source
theorem
LO
.
Modal
.
Hilbert
.
KD4_weakerThan_KD45
{α :
Type
u_1}
:
LO.Modal.Hilbert.KD4
α
≤ₛ
LO.Modal.Hilbert.KD45
α
source
theorem
LO
.
Modal
.
Hilbert
.
KD4_strictlyWeakerThan_KD45
:
LO.Modal.Hilbert.KD4
ℕ
<ₛ
LO.Modal.Hilbert.KD45
ℕ