Documentation

LeanPool.Incompleteness.Foundation.Modal.Kripke.AxiomVer

AxiomVer #

source
@[reducible, inline]
abbrev LO.Modal.Kripke.IsolatedFrameClass :
FrameClass

Imported declaration from the Incompleteness formalization.

Equations
Instances For
    source
    instance LO.Modal.Kripke.instIsNonemptyIsolatedFrameClass :
    IsolatedFrameClass.IsNonempty
    source
    instance LO.Modal.Kripke.IsolatedFrameClass.DefinedByAxiomVer :
    IsolatedFrameClass.DefinedByFormula (Axioms.Ver (Formula.atom 0))