@[reducible, inline]
Equations
- LO.Modal.Kripke.Frame.RelReflTransGen = Relation.ReflTransGen fun (x1 x2 : F.World) => x1 ≺ x2
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.Modal.Kripke.Frame.RelReflTransGen.single
{F : LO.Modal.Kripke.Frame}
{x y : F.World}
(hxy : x ≺ y)
:
x ≺^* y
@[simp]
theorem
LO.Modal.Kripke.Frame.RelReflTransGen.reflexive
{F : LO.Modal.Kripke.Frame}
:
Reflexive LO.Modal.Kripke.Frame.RelReflTransGen
@[simp]
theorem
LO.Modal.Kripke.Frame.RelReflTransGen.refl
{F : LO.Modal.Kripke.Frame}
{x : F.World}
:
x ≺^* x
@[simp]
theorem
LO.Modal.Kripke.Frame.RelReflTransGen.transitive
{F : LO.Modal.Kripke.Frame}
:
Transitive LO.Modal.Kripke.Frame.RelReflTransGen
@[simp]
@[reducible, inline]
Equations
- F^* = LO.Modal.Kripke.Frame.mk F.World fun (x1 x2 : F.World) => x1 ≺^* x2
Instances For
Equations
- LO.Modal.Kripke.«term_^*» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.«term_^*» 95 95 (Lean.ParserDescr.symbol "^*")
Instances For
theorem
LO.Modal.Kripke.Frame.TransitiveReflexiveClosure.single
{F : LO.Modal.Kripke.Frame}
{x y : F.World}
(hxy : x ≺ y)
:
F^*.Rel x y
@[reducible, inline]
Equations
- LO.Modal.Kripke.Frame.RelTransGen = Relation.TransGen fun (x1 x2 : F.World) => x1 ≺ x2
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.Modal.Kripke.Frame.RelTransGen.single
{F : LO.Modal.Kripke.Frame}
{x y : F.World}
(hxy : x ≺ y)
:
x ≺^+ y
@[simp]
theorem
LO.Modal.Kripke.Frame.RelTransGen.transitive
{F : LO.Modal.Kripke.Frame}
:
Transitive LO.Modal.Kripke.Frame.RelTransGen
@[simp]
theorem
LO.Modal.Kripke.Frame.RelTransGen.symmetric
{F : LO.Modal.Kripke.Frame}
(hSymm : Symmetric F.Rel)
:
Symmetric LO.Modal.Kripke.Frame.RelTransGen
@[reducible, inline]
Equations
- F^+ = LO.Modal.Kripke.Frame.mk F.World fun (x1 x2 : F.World) => x1 ≺^+ x2
Instances For
Equations
- LO.Modal.Kripke.«term_^+» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.«term_^+» 95 95 (Lean.ParserDescr.symbol "^+")
Instances For
theorem
LO.Modal.Kripke.Frame.TransitiveClosure.single
{F : LO.Modal.Kripke.Frame}
{x y : F.World}
(hxy : x ≺ y)
:
F^+.Rel x y
theorem
LO.Modal.Kripke.Frame.TransitiveClosure.rel_symmetric
{F : LO.Modal.Kripke.Frame}
(hSymm : Symmetric F.Rel)
:
@[reducible, inline]
Equations
- LO.Modal.Kripke.Frame.RelReflGen = Relation.ReflGen fun (x1 x2 : F.World) => x1 ≺ x2
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
Equations
- F^= = LO.Modal.Kripke.Frame.mk F.World fun (x1 x2 : F.World) => LO.Modal.Kripke.Frame.RelReflGen x1 x2
Instances For
Equations
- LO.Modal.Kripke.«term_^=» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.«term_^=» 95 95 (Lean.ParserDescr.symbol "^=")
Instances For
@[reducible, inline]
Equations
- LO.Modal.Kripke.Frame.RelIrreflGen = Relation.IrreflGen fun (x1 x2 : F.World) => x1 ≺ x2
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LO.Modal.Kripke.Frame.RelIrreflGen.rel_irreflexive
{F : LO.Modal.Kripke.Frame}
:
Irreflexive LO.Modal.Kripke.Frame.RelIrreflGen
@[reducible, inline]
Equations
- F^≠ = LO.Modal.Kripke.Frame.mk F.World fun (x1 x2 : F.World) => LO.Modal.Kripke.Frame.RelIrreflGen x1 x2
Instances For
Equations
- LO.Modal.Kripke.«term_^≠» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.«term_^≠» 95 95 (Lean.ParserDescr.symbol "^≠")
Instances For
@[simp]
theorem
LO.Modal.Kripke.Frame.IrreflexiveClosure.rel_irreflexive
{F : LO.Modal.Kripke.Frame}
:
Irreflexive F^≠.Rel