@[reducible, inline]

abbrev LO.Modal.Kripke.GLCompleteFrame {α : Type u} [Inhabited α] [DecidableEq α] (p : LO.Modal.Formula α) : LO.Kripke.FiniteFrame

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Modal.Kripke.GLCompleteFrame.irreflexive {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Formula α} : Irreflexive (LO.Modal.Kripke.GLCompleteFrame p).Rel

theorem LO.Modal.Kripke.GLCompleteFrame.transitive {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Formula α} : Transitive (LO.Modal.Kripke.GLCompleteFrame p).Rel

@[reducible, inline]

abbrev LO.Modal.Kripke.GLCompleteModel {α : Type u} [Inhabited α] [DecidableEq α] (p : LO.Modal.Formula α) : LO.Kripke.Model α

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Modal.Kripke.GL_truthlemma {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {X : (LO.Modal.Kripke.GLCompleteModel p).World} (q_sub : q ∈ 𝒮 p) : LO.Modal.Formula.Kripke.Satisfies (LO.Modal.Kripke.GLCompleteModel p) X q ↔ q ∈ X.formulae

instance LO.Modal.Kripke.GL_complete {α : Type u} [Inhabited α] [DecidableEq α] : LO.Complete 𝐆𝐋 LO.Kripke.TransitiveIrreflexiveFrameClassꟳ#α

Equations

• ⋯ = ⋯

instance LO.Modal.Kripke.instFiniteFramePropertyGLTransitiveIrreflexiveFrameClass {α : Type u} [Inhabited α] [DecidableEq α] : LO.Modal.Kripke.FiniteFrameProperty 𝐆𝐋 LO.Kripke.TransitiveIrreflexiveFrameClass

Equations

• LO.Modal.Kripke.instFiniteFramePropertyGLTransitiveIrreflexiveFrameClass = LO.Modal.Kripke.FiniteFrameProperty.mk