Foundation.Modal.Kripke.Closure

source

@[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

Instances For

source

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

Lean.TrailingParserDescr

Equations

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

Instances For

source

@[simp]

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

x ≺^* y

source

@[simp]

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

Reflexive RelReflTransGen

source

@[simp]

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

x ≺^* x

source

@[simp]

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

Transitive RelReflTransGen

source

@[simp]

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

Symmetric F.Rel → Symmetric RelReflTransGen

source

@[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

Instances For

source

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

Lean.TrailingParserDescr

Equations

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

Instances For

source

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

F^*.Rel x y

source

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

Reflexive F^*.Rel

source

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

Transitive F^*.Rel

source

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

Symmetric F.Rel → Symmetric F^*.Rel

source

@[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

Instances For

source

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

Lean.TrailingParserDescr

Equations

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

Instances For

source

@[simp]

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

x ≺^+ y

source

@[simp]

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

Transitive RelTransGen

source

@[simp]

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

Symmetric RelTransGen

source

@[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

Instances For

source

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

Lean.TrailingParserDescr

Equations

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

Instances For

source

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

F^+.Rel x y

source

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

Transitive F^+.Rel

source

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

Symmetric F^+.Rel

source

@[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

Instances For

source

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

Lean.TrailingParserDescr

Equations

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

Instances For

source

@[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

Instances For

source

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

Lean.TrailingParserDescr

Equations

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

Instances For

source

@[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

Instances For

source

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

Lean.TrailingParserDescr

Equations

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

Instances For

source

@[simp]

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

Irreflexive Frame.RelIrreflGen

source

@[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

Instances For

source

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

Lean.TrailingParserDescr

Equations

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

Instances For

source

@[simp]

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

Irreflexive F^≠.Rel