@[reducible, inline]
Equations
Instances For
instance
LO.Modal.Standard.Kripke.instSoundDeductionParameterFormulaDepVerAltIsolatedFrameClass
{α : Type u}
:
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
theorem
LO.Modal.Standard.Kripke.isolated_CanonicalFrame
{α : Type u}
[DecidableEq α]
{Ax : LO.Modal.Standard.AxiomSet α}
(h : 𝗩𝗲𝗿 ⊆ Ax)
[LO.System.Consistent 𝝂Ax]
:
instance
LO.Modal.Standard.Kripke.instCompleteDeductionParameterFormulaDepVerAltIsolatedFrameClass
{α : Type u}
[DecidableEq α]
:
Equations
- ⋯ = ⋯