Documentation

Foundation.Modal.Hilbert.WeakerThan.KB5_S5

source
theorem LO.Modal.Hilbert.KB5_weakerThan_S5 :
Hilbert.KB5 ℕ ≤ₛ Hilbert.S5 ℕ
source
theorem LO.Modal.Hilbert.KB5_strictlyWeakerThan_S5 :
Hilbert.KB5 ℕ <ₛ Hilbert.S5 ℕ