Closure

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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} : Std.Refl 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} : IsTrans F.World RelReflTransGen

@[simp]

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

• F^* = { World := F.World, Rel := fun (x1 x2 : F.World) => x1 ≺^* x2, world_nonempty := ⋯ }

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

Imported declaration from the Incompleteness formalization.

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} : Std.Refl F^*.Rel

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

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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} : IsTrans F.World RelTransGen

@[simp]

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

• F^+ = { World := F.World, Rel := fun (x1 x2 : F.World) => x1 ≺^+ x2, world_nonempty := ⋯ }

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

Imported declaration from the Incompleteness formalization.

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} : IsTrans F^+.World F^+.Rel

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

• F^= = { World := F.World, Rel := fun (x1 x2 : F.World) => LO.Modal.Kripke.Frame.RelReflGen x1 x2, world_nonempty := ⋯ }

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

• F^≠ = { World := F.World, Rel := fun (x1 x2 : F.World) => LO.Modal.Kripke.Frame.RelIrreflGen x1 x2, world_nonempty := ⋯ }

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

Imported declaration from the Incompleteness formalization.

Equations

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

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