Foundation.Logic.Kripke.Closure

source

@[reducible, inline]

abbrev LO.Kripke.Frame.RelReflTransGen {F : LO.Kripke.Frame} :

Rel F.World F.World

Equations

LO.Kripke.Frame.RelReflTransGen = Relation.ReflTransGen fun (x x_1 : F.World) => x ≺ x_1

Instances For

source

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

Lean.TrailingParserDescr

Equations

LO.Kripke.«term_≺^*_» = Lean.ParserDescr.trailingNode `LO.Kripke.term_≺^*_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≺^* ") (Lean.ParserDescr.cat `term 46))

Instances For

source

@[simp]

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

x ≺^* y

source

@[simp]

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

Reflexive LO.Kripke.Frame.RelReflTransGen

source

@[simp]

theorem LO.Kripke.Frame.RelReflTransGen.refl {F : LO.Kripke.Frame} {x : F.World} :

x ≺^* x

source

@[simp]

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

Transitive LO.Kripke.Frame.RelReflTransGen

source

@[simp]

theorem LO.Kripke.Frame.RelReflTransGen.symmetric {F : LO.Kripke.Frame} :

Symmetric F.Rel → Symmetric LO.Kripke.Frame.RelReflTransGen

source

@[reducible, inline]

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

LO.Kripke.Frame

Equations

F^* = LO.Kripke.Frame.mk F.World fun (x x_1 : F.World) => x ≺^* x_1

Instances For

source

def LO.Kripke.«term_^*» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

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

F^*.Rel x y

source

theorem LO.Kripke.Frame.TransitiveReflexiveClosure.rel_reflexive {F : LO.Kripke.Frame} :

Reflexive F^*.Rel

source

theorem LO.Kripke.Frame.TransitiveReflexiveClosure.rel_transitive {F : LO.Kripke.Frame} :

Transitive F^*.Rel

source

theorem LO.Kripke.Frame.TransitiveReflexiveClosure.rel_symmetric {F : LO.Kripke.Frame} :

Symmetric F.Rel → Symmetric F^*.Rel

source

@[reducible, inline]

abbrev LO.Kripke.Frame.RelTransGen {F : LO.Kripke.Frame} :

Rel F.World F.World

Equations

LO.Kripke.Frame.RelTransGen = Relation.TransGen fun (x x_1 : F.World) => x ≺ x_1

Instances For

source

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

Lean.TrailingParserDescr

Equations

LO.Kripke.«term_≺^+_» = Lean.ParserDescr.trailingNode `LO.Kripke.term_≺^+_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≺^+ ") (Lean.ParserDescr.cat `term 46))

Instances For

source

@[simp]

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

x ≺^+ y

source

@[simp]

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

Transitive LO.Kripke.Frame.RelTransGen

source

@[simp]

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

Symmetric LO.Kripke.Frame.RelTransGen

source

@[reducible, inline]

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

LO.Kripke.Frame

Equations

F^+ = LO.Kripke.Frame.mk F.World fun (x x_1 : F.World) => x ≺^+ x_1

Instances For

source

def LO.Kripke.«term_^+» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

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

F^+.Rel x y

source

theorem LO.Kripke.Frame.TransitiveClosure.rel_transitive {F : LO.Kripke.Frame} :

Transitive F^+.Rel

source

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

Symmetric F^+.Rel

source

@[reducible, inline]

abbrev LO.Kripke.Frame.RelReflGen {F : LO.Kripke.Frame} :

Rel F.World F.World

Equations

LO.Kripke.Frame.RelReflGen = Relation.ReflGen fun (x x_1 : F.World) => x ≺ x_1

Instances For

source

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

Lean.TrailingParserDescr

Equations

LO.Kripke.«term_≺^=_» = Lean.ParserDescr.trailingNode `LO.Kripke.term_≺^=_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≺^= ") (Lean.ParserDescr.cat `term 46))

Instances For

source

@[reducible, inline]

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

LO.Kripke.Frame

Equations

F^= = LO.Kripke.Frame.mk F.World fun (x x_1 : F.World) => LO.Kripke.Frame.RelReflGen x x_1

Instances For

source

def LO.Kripke.«term_^=» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

@[reducible, inline]

abbrev LO.Kripke.Frame.RelIrreflGen {F : LO.Kripke.Frame} :

Rel F.World F.World

Equations

LO.Kripke.Frame.RelIrreflGen = Relation.IrreflGen fun (x x_1 : F.World) => x ≺ x_1

Instances For

source

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

Lean.TrailingParserDescr

Equations

LO.Kripke.«term_≺^≠_» = Lean.ParserDescr.trailingNode `LO.Kripke.term_≺^≠_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≺^≠ ") (Lean.ParserDescr.cat `term 46))

Instances For

source

@[simp]

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

Irreflexive LO.Kripke.Frame.RelIrreflGen

source

@[reducible, inline]

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

LO.Kripke.Frame

Equations

F^≠ = LO.Kripke.Frame.mk F.World fun (x x_1 : F.World) => LO.Kripke.Frame.RelIrreflGen x x_1

Instances For

source

def LO.Kripke.«term_^≠» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

@[simp]

theorem LO.Kripke.Frame.IrreflexiveClosure.rel_irreflexive {F : LO.Kripke.Frame} :

Irreflexive F^≠.Rel