Documentation

Foundation.Modal.Hilbert.WeakerThan.GL_GLS

source
theorem LO.Modal.Hilbert.GL_weakerThan_GLS {α : Type u_1} :
LO.Modal.Hilbert.GL α ≤ₛ LO.Modal.Hilbert.GLS α