Documentation

Foundation.Modal.Hilbert.WeakerThan.KT_Grz

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