Documentation

Foundation.Modal.Hilbert.WeakerThan.K4_Triv

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