@[reducible, inline]

noncomputable abbrev LO.Modal.Formula.GrzSubformulas {α : Type u} [DecidableEq α] (p : LO.Modal.Formula α) : LO.Modal.Formulae α

Equations

• 𝒮ᴳ p = 𝒮 p ∪ Finset.image (fun (q : LO.Modal.Formula α) => □(q ➝ □q)) (Finset.prebox (𝒮 p))

def LO.Modal.Formula.«term𝒮ᴳ_» : Lean.ParserDescr

Equations

• LO.Modal.Formula.«term𝒮ᴳ_» = Lean.ParserDescr.node `LO.Modal.Formula.term𝒮ᴳ_ 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝒮ᴳ ") (Lean.ParserDescr.cat `term 70))

@[simp]

theorem LO.Modal.Formula.GrzSubformulas.mem_self {α : Type u} [DecidableEq α] {p : LO.Modal.Formula α} : p ∈ 𝒮ᴳ p

theorem LO.Modal.Formula.GrzSubformulas.mem_boximpbox {α : Type u} [DecidableEq α] {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (h : q ∈ Finset.prebox (𝒮 p)) : □(q ➝ □q) ∈ 𝒮ᴳ p

theorem LO.Modal.Formula.GrzSubformulas.mem_origin {α : Type u} [DecidableEq α] {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (h : q ∈ 𝒮 p) : q ∈ 𝒮ᴳ p

theorem LO.Modal.Formula.GrzSubformulas.mem_imp {α : Type u} [DecidableEq α] {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} (h : q ➝ r ∈ 𝒮ᴳ p) : q ∈ 𝒮ᴳ p ∧ r ∈ 𝒮ᴳ p

theorem LO.Modal.Formula.GrzSubformulas.mem_imp₁ {α : Type u} [DecidableEq α] {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} (h : q ➝ r ∈ 𝒮ᴳ p) : q ∈ 𝒮ᴳ p

theorem LO.Modal.Formula.GrzSubformulas.mem_imp₂ {α : Type u} [DecidableEq α] {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} (h : q ➝ r ∈ 𝒮ᴳ p) : r ∈ 𝒮ᴳ p

@[reducible, inline]

abbrev LO.Modal.Kripke.GrzCompleteFrame {α : 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.GrzCompleteFrame.reflexive {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Formula α} : Reflexive (LO.Modal.Kripke.GrzCompleteFrame p).Rel

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

theorem LO.Modal.Kripke.GrzCompleteFrame.antisymm {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Formula α} : Antisymmetric (LO.Modal.Kripke.GrzCompleteFrame p).Rel

@[reducible, inline]

abbrev LO.Modal.Kripke.GrzCompleteModel {α : 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.Grz_truthlemma {α : Type u} [Inhabited α] [DecidableEq α] {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {X : (LO.Modal.Kripke.GrzCompleteModel p).World} (q_sub : q ∈ 𝒮 p) : LO.Modal.Formula.Kripke.Satisfies (LO.Modal.Kripke.GrzCompleteModel p) X q ↔ q ∈ X.formulae

instance LO.Modal.Kripke.Grz_complete {α : Type u} [Inhabited α] [DecidableEq α] : LO.Complete 𝐆𝐫𝐳 LO.Kripke.ReflexiveTransitiveAntisymmetricFrameClassꟳ#α

Equations

• ⋯ = ⋯

instance LO.Modal.Kripke.instFiniteFramePropertyGrzReflexiveTransitiveAntisymmetricFrameClass {α : Type u} [Inhabited α] [DecidableEq α] : LO.Modal.Kripke.FiniteFrameProperty 𝐆𝐫𝐳 LO.Kripke.ReflexiveTransitiveAntisymmetricFrameClass

Equations

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