Documentation

Foundation.Modal.System.Grz

noncomputable def LO.System.Grz.lemma_axiomFour_axiomT {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓒 : S} [LO.System.Grz 𝓒] {Ο† : F} :
Equations
Instances For
    noncomputable def LO.System.Grz.axiomFour {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓒 : S} [LO.System.Grz 𝓒] {Ο† : F} :
    Equations
    Instances For
      noncomputable instance LO.System.Grz.instHasAxiomFour {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓒 : S} [LO.System.Grz 𝓒] :
      Equations
      • LO.System.Grz.instHasAxiomFour = { Four := fun (x : F) => LO.System.Grz.axiomFour }
      noncomputable def LO.System.Grz.axiomT {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓒 : S} [LO.System.Grz 𝓒] {Ο† : F} :
      𝓒 ⊒ β–‘Ο† ➝ Ο†
      Equations
      Instances For
        noncomputable instance LO.System.Grz.instHasAxiomT {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓒 : S} [LO.System.Grz 𝓒] :
        Equations
        • LO.System.Grz.instHasAxiomT = { T := fun (x : F) => LO.System.Grz.axiomT }