@[reducible, inline]

abbrev LO.Modal.Kripke.Frame.RelReflTransGen {F : Frame} : _root_.Rel F.World F.World

Equations

• LO.Modal.Kripke.Frame.RelReflTransGen = Relation.ReflTransGen fun (x1 x2 : F.World) => x1 ≺ x2

def LO.Modal.Kripke.«term_≺^*_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LO.Modal.Kripke.Frame.RelReflTransGen.single {F : Frame} {x y : F.World} (hxy : x ≺ y) : x ≺^* y

@[simp]

theorem LO.Modal.Kripke.Frame.RelReflTransGen.reflexive {F : Frame} : Reflexive RelReflTransGen

@[simp]

theorem LO.Modal.Kripke.Frame.RelReflTransGen.refl {F : Frame} {x : F.World} : x ≺^* x

@[simp]

theorem LO.Modal.Kripke.Frame.RelReflTransGen.transitive {F : Frame} : Transitive RelReflTransGen

@[simp]

theorem LO.Modal.Kripke.Frame.RelReflTransGen.symmetric {F : Frame} : Symmetric F.Rel → Symmetric RelReflTransGen

@[reducible, inline]

abbrev LO.Modal.Kripke.Frame.TransitiveReflexiveClosure (F : Frame) : Frame

Equations

• F^* = LO.Modal.Kripke.Frame.mk F.World fun (x1 x2 : F.World) => x1 ≺^* x2

def LO.Modal.Kripke.«term_^*» : Lean.TrailingParserDescr

Equations

• LO.Modal.Kripke.«term_^*» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.«term_^*» 95 95 (Lean.ParserDescr.symbol "^*")

theorem LO.Modal.Kripke.Frame.TransitiveReflexiveClosure.single {F : Frame} {x y : F.World} (hxy : x ≺ y) : F^*.Rel x y

theorem LO.Modal.Kripke.Frame.TransitiveReflexiveClosure.rel_reflexive {F : Frame} : Reflexive F^*.Rel

theorem LO.Modal.Kripke.Frame.TransitiveReflexiveClosure.rel_transitive {F : Frame} : Transitive F^*.Rel

theorem LO.Modal.Kripke.Frame.TransitiveReflexiveClosure.rel_symmetric {F : Frame} : Symmetric F.Rel → Symmetric F^*.Rel

@[reducible, inline]

abbrev LO.Modal.Kripke.Frame.RelTransGen {F : Frame} : _root_.Rel F.World F.World

Equations

• LO.Modal.Kripke.Frame.RelTransGen = Relation.TransGen fun (x1 x2 : F.World) => x1 ≺ x2

def LO.Modal.Kripke.«term_≺^+_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LO.Modal.Kripke.Frame.RelTransGen.single {F : Frame} {x y : F.World} (hxy : x ≺ y) : x ≺^+ y

@[simp]

theorem LO.Modal.Kripke.Frame.RelTransGen.transitive {F : Frame} : Transitive RelTransGen

@[simp]

theorem LO.Modal.Kripke.Frame.RelTransGen.symmetric {F : Frame} (hSymm : Symmetric F.Rel) : Symmetric RelTransGen

@[reducible, inline]

abbrev LO.Modal.Kripke.Frame.TransitiveClosure (F : Frame) : Frame

Equations

• F^+ = LO.Modal.Kripke.Frame.mk F.World fun (x1 x2 : F.World) => x1 ≺^+ x2

def LO.Modal.Kripke.«term_^+» : Lean.TrailingParserDescr

Equations

• LO.Modal.Kripke.«term_^+» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.«term_^+» 95 95 (Lean.ParserDescr.symbol "^+")

theorem LO.Modal.Kripke.Frame.TransitiveClosure.single {F : Frame} {x y : F.World} (hxy : x ≺ y) : F^+.Rel x y

theorem LO.Modal.Kripke.Frame.TransitiveClosure.rel_transitive {F : Frame} : Transitive F^+.Rel

theorem LO.Modal.Kripke.Frame.TransitiveClosure.rel_symmetric {F : Frame} (hSymm : Symmetric F.Rel) : Symmetric F^+.Rel

@[reducible, inline]

abbrev LO.Modal.Kripke.Frame.RelReflGen {F : Frame} : _root_.Rel F.World F.World

Equations

• LO.Modal.Kripke.Frame.RelReflGen = Relation.ReflGen fun (x1 x2 : F.World) => x1 ≺ x2

def LO.Modal.Kripke.«term_≺^=_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev LO.Modal.Kripke.Frame.ReflexiveClosure (F : Frame) : Frame

Equations

• F^= = LO.Modal.Kripke.Frame.mk F.World fun (x1 x2 : F.World) => LO.Modal.Kripke.Frame.RelReflGen x1 x2

def LO.Modal.Kripke.«term_^=» : Lean.TrailingParserDescr

Equations

• LO.Modal.Kripke.«term_^=» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.«term_^=» 95 95 (Lean.ParserDescr.symbol "^=")

@[reducible, inline]

abbrev LO.Modal.Kripke.Frame.RelIrreflGen {F : Frame} : _root_.Rel F.World F.World

Equations

• LO.Modal.Kripke.Frame.RelIrreflGen = Relation.IrreflGen fun (x1 x2 : F.World) => x1 ≺ x2

def LO.Modal.Kripke.«term_≺^≠_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LO.Modal.Kripke.Frame.RelIrreflGen.rel_irreflexive {F : Frame} : Irreflexive Frame.RelIrreflGen

@[reducible, inline]

abbrev LO.Modal.Kripke.Frame.IrreflexiveClosure (F : Frame) : Frame

Equations

• F^≠ = LO.Modal.Kripke.Frame.mk F.World fun (x1 x2 : F.World) => LO.Modal.Kripke.Frame.RelIrreflGen x1 x2

def LO.Modal.Kripke.«term_^≠» : Lean.TrailingParserDescr

Equations

• LO.Modal.Kripke.«term_^≠» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.«term_^≠» 95 95 (Lean.ParserDescr.symbol "^≠")

@[simp]

theorem LO.Modal.Kripke.Frame.IrreflexiveClosure.rel_irreflexive {F : Frame} : Irreflexive F^≠.Rel