Documentation

Foundation.Modal.Hilbert.WeakerThan.KD45_S5

source
theorem LO.Modal.Hilbert.KD45_weakerThan_S5 :
Hilbert.KD45 ℕ ≤ₛ Hilbert.S5 ℕ
source
theorem LO.Modal.Hilbert.KD45_strictlyWeakerThan_S5 :
Hilbert.KD45 ℕ <ₛ Hilbert.S5 ℕ