Documentation
Foundation
.
Modal
.
Kripke
.
Logic
.
GLPoint3
Search
return to top
source
Imports
Init
Foundation.Modal.Kripke.Logic.K4Point3
Foundation.Modal.Kripke.Logic.GL.Completeness
Imported by
LO
.
Modal
.
Kripke
.
Frame
.
IsFiniteGLPoint3
LO
.
Modal
.
Kripke
.
FrameClass
.
finite_GLPoint3
LO
.
Modal
.
Kripke
.
instIsFiniteGLPoint3Blackpoint
LO
.
Modal
.
Hilbert
.
GLPoint3
.
Kripke
.
instSoundNormalNatFormulaFrameClassFinite_GLPoint3
LO
.
Modal
.
Hilbert
.
GLPoint3
.
Kripke
.
instConsistentFormulaNatNormal
LO
.
Modal
.
Hilbert
.
GLPoint3
.
Kripke
.
instCompleteNormalNatFormulaFrameClassFinite_GLPoint3
LO
.
Modal
.
Hilbert
.
GLPoint3
.
Kripke
.
instStrictlyWeakerThanFormulaNatNormalGL
LO
.
Modal
.
Hilbert
.
GLPoint3
.
Kripke
.
instStrictlyWeakerThanFormulaNatNormalK4Point3
LO
.
Modal
.
instStrictlyWeakerThanFormulaNatLogicGLGLPoint3
LO
.
Modal
.
instStrictlyWeakerThanFormulaNatLogicK4Point3GLPoint3
source
class
LO
.
Modal
.
Kripke
.
Frame
.
IsFiniteGLPoint3
(
F
:
Frame
)
extends
F
.
IsFiniteGL
,
IsPiecewiseConnected
F
.
Rel
:
Prop
world_finite
:
Finite
F
.
World
irrefl
(
a
:
F
.
World
)
:
¬
F
.
Rel
a
a
trans
(
a
b
c
:
F
.
World
)
:
F
.
Rel
a
b
→
F
.
Rel
b
c
→
F
.
Rel
a
c
p_connected
:
PiecewiseConnected
F
.
Rel
Instances
source
@[reducible, inline]
abbrev
LO
.
Modal
.
Kripke
.
FrameClass
.
finite_GLPoint3
:
FrameClass
Equations
LO.Modal.Kripke.FrameClass.finite_GLPoint3
=
{
F
:
LO.Modal.Kripke.Frame
|
F
.
IsFiniteGLPoint3
}
Instances For
source
instance
LO
.
Modal
.
Kripke
.
instIsFiniteGLPoint3Blackpoint
:
blackpoint
.
IsFiniteGLPoint3
source
instance
LO
.
Modal
.
Hilbert
.
GLPoint3
.
Kripke
.
instSoundNormalNatFormulaFrameClassFinite_GLPoint3
:
Sound
Hilbert.GLPoint3
Kripke.FrameClass.finite_GLPoint3
source
instance
LO
.
Modal
.
Hilbert
.
GLPoint3
.
Kripke
.
instConsistentFormulaNatNormal
:
Entailment.Consistent
Hilbert.GLPoint3
source
instance
LO
.
Modal
.
Hilbert
.
GLPoint3
.
Kripke
.
instCompleteNormalNatFormulaFrameClassFinite_GLPoint3
:
Complete
Hilbert.GLPoint3
Kripke.FrameClass.finite_GLPoint3
source
instance
LO
.
Modal
.
Hilbert
.
GLPoint3
.
Kripke
.
instStrictlyWeakerThanFormulaNatNormalGL
:
Hilbert.GL
⪱
Hilbert.GLPoint3
source
instance
LO
.
Modal
.
Hilbert
.
GLPoint3
.
Kripke
.
instStrictlyWeakerThanFormulaNatNormalK4Point3
:
Hilbert.K4Point3
⪱
Hilbert.GLPoint3
source
instance
LO
.
Modal
.
instStrictlyWeakerThanFormulaNatLogicGLGLPoint3
:
Modal.GL
⪱
Modal.GLPoint3
source
instance
LO
.
Modal
.
instStrictlyWeakerThanFormulaNatLogicK4Point3GLPoint3
:
Modal.K4Point3
⪱
Modal.GLPoint3