Documentation

Foundation.Modal.Hilbert.WeakerThan.K4_Grz

source
theorem LO.Modal.Hilbert.K4_weakerThan_Grz {α : Type u_1} [DecidableEq α] :
LO.Modal.Hilbert.K4 α ≤ₛ LO.Modal.Hilbert.Grz α