def
LO.Modal.Entailment.lem₁_diaT_of_S5Grz
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[Entailment F S]
{𝓢 : S}
[Entailment.S5 𝓢]
{φ : F}
:
def
LO.Modal.Entailment.lem₂_diaT_of_S5Grz
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[Entailment F S]
{𝓢 : S}
[DecidableEq F]
[Entailment.S5 𝓢]
{φ : F}
:
class
LO.Modal.Entailment.S5Grz
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[Entailment F S]
(𝓢 : S)
extends LO.Modal.Entailment.S5 𝓢, LO.Modal.Entailment.HasAxiomGrz 𝓢 :
Type (max u_2 u_3)
def
LO.Modal.Entailment.S5Grz.diaT
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[Entailment F S]
{𝓢 : S}
[DecidableEq F]
[Entailment.S5Grz 𝓢]
{φ : F}
:
Equations
- One or more equations did not get rendered due to their size.
instance
LO.Modal.Entailment.S5Grz.instHasAxiomDiaT
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[Entailment F S]
{𝓢 : S}
[DecidableEq F]
[Entailment.S5Grz 𝓢]
:
Equations
- LO.Modal.Entailment.S5Grz.instHasAxiomDiaT = { diaT := fun (x : F) => LO.Modal.Entailment.S5Grz.diaT }
instance
LO.Modal.Entailment.S5Grz.instKTc'
{S : Type u_1}
{F : Type u_2}
[BasicModalLogicalConnective F]
[Entailment F S]
{𝓢 : S}
[DecidableEq F]
[Entailment.S5Grz 𝓢]
:
Equations
- LO.Modal.Entailment.S5Grz.instKTc' = { toK := inst✝.toK, toHasAxiomDiaT := LO.Modal.Entailment.S5Grz.instHasAxiomDiaT }
@[reducible, inline]
Equations
- One or more equations did not get rendered due to their size.
Equations
- LO.Modal.Hilbert.S5Grz.instHasKNat = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.S5Grz.instHasKNat._proof_1, mem_K := LO.Modal.Hilbert.S5Grz.instHasKNat._proof_2 }
Equations
- LO.Modal.Hilbert.S5Grz.instHasTNat = { p := 0, mem_T := LO.Modal.Hilbert.S5Grz.instHasTNat._proof_1 }
Equations
- LO.Modal.Hilbert.S5Grz.instHasFiveNat = { p := 0, mem_Five := LO.Modal.Hilbert.S5Grz.instHasFiveNat._proof_1 }
Equations
- LO.Modal.Hilbert.S5Grz.instHasGrzNat = { p := 0, mem_Grz := LO.Modal.Hilbert.S5Grz.instHasGrzNat._proof_1 }
Equations
- One or more equations did not get rendered due to their size.
Equations
@[reducible, inline]