- toRel : Rel M₁.World M₂.World
Instances For
Equations
- LO.Modal.Kripke.«term_⇄_» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.«term_⇄_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇄ ") (Lean.ParserDescr.cat `term 81))
Instances For
Equations
- LO.Modal.Kripke.instCoeFunBisimulationForallWorldForallProp = { coe := fun (bi : M₁ ⇄ M₂) => bi.toRel }
Equations
- LO.Modal.Kripke.«term_↭_» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.«term_↭_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↭ ") (Lean.ParserDescr.cat `term 51))
Instances For
theorem
LO.Modal.Kripke.modal_equivalent_of_bisimilar
{M₁ M₂ : Model}
{x₁ : M₁.World}
{x₂ : M₂.World}
(Bi : M₁ ⇄ M₂)
(bisx : Bi.toRel x₁ x₂)
:
x₁ ↭ x₂
Equations
- LO.Modal.Kripke.«term_→ₚ_» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.«term_→ₚ_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ₚ ") (Lean.ParserDescr.cat `term 81))
Instances For
Equations
- LO.Modal.Kripke.instCoeFunPseudoEpimorphismForallWorld = { coe := fun (f : F₁ →ₚ F₂) => f.toFun }
Equations
- LO.Modal.Kripke.Frame.PseudoEpimorphism.id = { toFun := id, forth := ⋯, back := ⋯ }
Instances For
def
LO.Modal.Kripke.Frame.PseudoEpimorphism.TransitiveClosure
{F₁ F₂ : Frame}
(f : F₁ →ₚ F₂)
(F₂_trans : Transitive F₂.Rel)
:
Equations
- f.TransitiveClosure F₂_trans = { toFun := f.toFun, forth := ⋯, back := ⋯ }
Instances For
structure
LO.Modal.Kripke.Model.PseudoEpimorphism
(M₁ M₂ : Model)
extends M₁.toFrame →ₚ M₂.toFrame :
- toFun : M₁.World → M₂.World
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- LO.Modal.Kripke.instCoeFunPseudoEpimorphismForallWorld_1 = { coe := fun (f : M₁ →ₚ M₂) => f.toFun }
Equations
- LO.Modal.Kripke.Model.PseudoEpimorphism.id = { toFun := id, forth := ⋯, back := ⋯, atomic := ⋯ }
Instances For
def
LO.Modal.Kripke.Model.PseudoEpimorphism.mkAtomic
{M₁ M₂ : Model}
(f : M₁.toFrame →ₚ M₂.toFrame)
(atomic : ∀ {w : M₁.World} {a : ℕ}, M₁.Val w a ↔ M₂.Val (f.toFun w) a)
:
M₁ →ₚ M₂
Equations
- LO.Modal.Kripke.Model.PseudoEpimorphism.mkAtomic f atomic = { toFun := f.toFun, forth := ⋯, back := ⋯, atomic := ⋯ }
Instances For
def
LO.Modal.Kripke.Model.PseudoEpimorphism.comp
{M₁ M₂ M₃ : Model}
(f : M₁ →ₚ M₂)
(g : M₂ →ₚ M₃)
:
M₁ →ₚ M₃
Equations
- f.comp g = LO.Modal.Kripke.Model.PseudoEpimorphism.mkAtomic (f.comp g.toPseudoEpimorphism) ⋯
Instances For
Equations
- f.bisimulation = { toRel := Function.graph f.toFun, atomic := ⋯, forth := ⋯, back := ⋯ }
Instances For
theorem
LO.Modal.Kripke.Model.PseudoEpimorphism.modal_equivalence
{M₁ M₂ : Model}
(f : M₁ →ₚ M₂)
(w : M₁.World)
:
w ↭ f.toFun w
theorem
LO.Modal.Kripke.iff_formula_valid_on_frame_surjective_morphism
{F₁ F₂ : Frame}
{φ : Formula ℕ}
(f : F₁ →ₚ F₂)
(f_surjective : Function.Surjective f.toFun)
:
theorem
LO.Modal.Kripke.iff_theory_valid_on_frame_surjective_morphism
{F₁ F₂ : Frame}
{T : Set (Formula ℕ)}
(f : F₁ →ₚ F₂)
(f_surjective : Function.Surjective f.toFun)
:
- Rel : _root_.Rel self.World self.World
- world_nonempty : Nonempty self.World
- root : self.World
- root_rooted : self.isRooted self.root
- default : self.World
Instances For
Equations
Instances For
Equations
- LO.Modal.Kripke.«term_↾_» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.«term_↾_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↾") (Lean.ParserDescr.cat `term 101))
Instances For
theorem
LO.Modal.Kripke.Frame.PointGenerated.rel_transitive
{F : Frame}
{r : F.World}
(F_trans : Transitive F.Rel)
:
Transitive (F↾r).Rel
theorem
LO.Modal.Kripke.Frame.PointGenerated.rel_irreflexive
{F : Frame}
{r : F.World}
(F_irrefl : Irreflexive F.Rel)
:
Irreflexive (F↾r).Rel
instance
LO.Modal.Kripke.Frame.PointGenerated.instDecidableEqWorld
{F : Frame}
{r : F.World}
[DecidableEq F.World]
:
DecidableEq (F↾r).World
structure
LO.Modal.Kripke.RootedModelextends LO.Modal.Kripke.Model, LO.Modal.Kripke.RootedFrame :
Type 1
- Rel : _root_.Rel self.World self.World
- world_nonempty : Nonempty self.World
- root : self.World
- root_rooted : self.isRooted self.root
- default : self.World
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Modal.Kripke.Model.PointGenerated.bisimulation_of_trans
{M : Model}
(M_trans : Transitive M.Rel)
(r : M.World)
:
Equations
- LO.Modal.Kripke.Model.PointGenerated.bisimulation_of_trans M_trans r = { toRel := fun (x : (M↾r).World) (y : M.World) => ↑x = y, atomic := ⋯, forth := ⋯, back := ⋯ }
Instances For
theorem
LO.Modal.Kripke.Model.PointGenerated.modal_equivalent_at_root
{M : Model}
(M_trans : Transitive M.Rel)
(r : M.World)
:
⟨r, ⋯⟩ ↭ r
- toFun : F₁.World → F₂.World
- monic : Function.Injective self.toFun
Instances For
Equations
- LO.Modal.Kripke.«term_⊆ₚ_» = Lean.ParserDescr.trailingNode `LO.Modal.Kripke.«term_⊆ₚ_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊆ₚ ") (Lean.ParserDescr.cat `term 81))
Instances For
@[reducible, inline]
Equations
Instances For
theorem
LO.Modal.Kripke.undefinable_irreflexive :
¬∃ (Ax : Theory ℕ), IrreflexiveFrameClass.DefinedBy Ax