@[reducible, inline]

abbrev LO.Modal.Kripke.TransitiveConverseWellFoundedFrameClass : FrameClass

Equations

• LO.Modal.Kripke.TransitiveConverseWellFoundedFrameClass = {F : LO.Modal.Kripke.Frame | Transitive F.Rel ∧ ConverseWellFounded F.Rel}

@[reducible, inline]

abbrev LO.Modal.Kripke.TransitiveIrreflexiveFiniteFrameClass : FiniteFrameClass

Equations

• LO.Modal.Kripke.TransitiveIrreflexiveFiniteFrameClass = {F : LO.Modal.Kripke.FiniteFrame | Transitive F.Rel ∧ Irreflexive F.Rel}

theorem LO.Modal.Kripke.TransitiveConverseWellFoundedFrameClass.is_defined_by_L : TransitiveConverseWellFoundedFrameClass.DefinedBy 𝗟

theorem LO.Modal.Kripke.FiniteIrreflexiveFrameClass.is_finite_defined_by_L : TransitiveIrreflexiveFiniteFrameClass.DefinedBy 𝗟

instance LO.Modal.Hilbert.GL.Kripke.sound : Sound (Hilbert.GL ℕ) Kripke.TransitiveConverseWellFoundedFrameClass

instance LO.Modal.Hilbert.GL.Kripke.finite_sound : Sound (Hilbert.GL ℕ) Kripke.TransitiveIrreflexiveFiniteFrameClass

instance LO.Modal.Hilbert.GL.consistent : System.Consistent (Hilbert.GL ℕ)