Documentation

Foundation.Modal.Hilbert.Equiv.KD_KP

source
theorem LO.Modal.Hilbert.KD_weakerThan_KP {α : Type u_1} [DecidableEq α] :
LO.Modal.Hilbert.KD α ≤ₛ LO.Modal.Hilbert.KP α
source
theorem LO.Modal.Hilbert.KP_weakerThan_KD {α : Type u_1} [DecidableEq α] :
LO.Modal.Hilbert.KP α ≤ₛ LO.Modal.Hilbert.KD α
source
theorem LO.Modal.Hilbert.KD_equiv_KP {α : Type u_1} [DecidableEq α] :
LO.Modal.Hilbert.KD α =ₛ LO.Modal.Hilbert.KP α