structure LO.Modal.Kripke.Model.Bisimulation (M₁ M₂ : LO.Modal.Kripke.Model) : Type

• toRel : Rel M₁.World M₂.World
• atomic : ∀ {x₁ : M₁.World} {x₂ : M₂.World} {a : ℕ}, self.toRel x₁ x₂ → (M₁.Val x₁ a ↔ M₂.Val x₂ a)
• forth : ∀ {x₁ y₁ : M₁.World} {x₂ : M₂.World}, self.toRel x₁ x₂ → x₁ ≺ y₁ → ∃ (y₂ : M₂.World), self.toRel y₁ y₂ ∧ x₂ ≺ y₂
• back : ∀ {x₁ : M₁.World} {x₂ y₂ : M₂.World}, self.toRel x₁ x₂ → x₂ ≺ y₂ → ∃ (y₁ : M₁.World), self.toRel y₁ y₂ ∧ x₁ ≺ y₁

def LO.Modal.Kripke.«term_⇄_» : Lean.TrailingParserDescr

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))

instance LO.Modal.Kripke.instCoeFunBisimulationForallWorldForallProp {M₁ M₂ : LO.Modal.Kripke.Model} : CoeFun (M₁ ⇄ M₂) fun (x : M₁ ⇄ M₂) => M₁.World → M₂.World → Prop

Equations

• LO.Modal.Kripke.instCoeFunBisimulationForallWorldForallProp = { coe := fun (bi : M₁ ⇄ M₂) => bi.toRel }

def LO.Modal.Kripke.ModalEquivalent {M₁ M₂ : LO.Modal.Kripke.Model} (w₁ : M₁.World) (w₂ : M₂.World) : Prop

Equations

• (w₁ ↭ w₂) = ∀ {φ : LO.Modal.Formula ℕ}, w₁ ⊧ φ ↔ w₂ ⊧ φ

def LO.Modal.Kripke.«term_↭_» : Lean.TrailingParserDescr

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))

theorem LO.Modal.Kripke.modal_equivalent_of_bisimilar {M₁ M₂ : LO.Modal.Kripke.Model} {x₁ : M₁.World} {x₂ : M₂.World} (Bi : M₁ ⇄ M₂) (bisx : Bi.toRel x₁ x₂) : x₁ ↭ x₂

structure LO.Modal.Kripke.Frame.PseudoEpimorphism (F₁ F₂ : LO.Modal.Kripke.Frame) : Type

• toFun : F₁.World → F₂.World
• forth : ∀ {x y : F₁.World}, x ≺ y → self.toFun x ≺ self.toFun y
• back : ∀ {w : F₁.World} {v : F₂.World}, self.toFun w ≺ v → ∃ (u : F₁.World), self.toFun u = v ∧ w ≺ u

def LO.Modal.Kripke.«term_→ₚ_» : Lean.TrailingParserDescr

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))

instance LO.Modal.Kripke.instCoeFunPseudoEpimorphismForallWorld {F₁ F₂ : LO.Modal.Kripke.Frame} : CoeFun (F₁ →ₚ F₂) fun (x : F₁ →ₚ F₂) => F₁.World → F₂.World

Equations

• LO.Modal.Kripke.instCoeFunPseudoEpimorphismForallWorld = { coe := fun (f : F₁ →ₚ F₂) => f.toFun }

def LO.Modal.Kripke.Frame.PseudoEpimorphism.id {F : LO.Modal.Kripke.Frame} : F →ₚ F

Equations

• LO.Modal.Kripke.Frame.PseudoEpimorphism.id = { toFun := id, forth := ⋯, back := ⋯ }

def LO.Modal.Kripke.Frame.PseudoEpimorphism.TransitiveClosure {F₁ F₂ : LO.Modal.Kripke.Frame} (f : F₁ →ₚ F₂) (F₂_trans : Transitive F₂.Rel) : F₁^+ →ₚ F₂

Equations

• f.TransitiveClosure F₂_trans = { toFun := f.toFun, forth := ⋯, back := ⋯ }

def LO.Modal.Kripke.Frame.PseudoEpimorphism.comp {F₁ F₂ F₃ : LO.Modal.Kripke.Frame} (f : F₁ →ₚ F₂) (g : F₂ →ₚ F₃) : F₁ →ₚ F₃

Equations

• f.comp g = { toFun := g.toFun ∘ f.toFun, forth := ⋯, back := ⋯ }

structure LO.Modal.Kripke.Model.PseudoEpimorphism (M₁ M₂ : LO.Modal.Kripke.Model) extends M₁.toFrame →ₚ M₂.toFrame : Type

• toFun : M₁.World → M₂.World
• forth : ∀ {x y : M₁.World}, x ≺ y → self.toFun x ≺ self.toFun y
• back : ∀ {w : M₁.World} {v : M₂.World}, self.toFun w ≺ v → ∃ (u : M₁.World), self.toFun u = v ∧ w ≺ u
• atomic : ∀ {a : ℕ} {w : M₁.World}, M₁.Val w a ↔ M₂.Val (self.toFun w) a

def LO.Modal.Kripke.«term_→ₚ__1» : Lean.TrailingParserDescr

Equations

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

instance LO.Modal.Kripke.instCoeFunPseudoEpimorphismForallWorld_1 {M₁ M₂ : LO.Modal.Kripke.Model} : CoeFun (M₁ →ₚ M₂) fun (x : M₁ →ₚ M₂) => M₁.World → M₂.World

Equations

• LO.Modal.Kripke.instCoeFunPseudoEpimorphismForallWorld_1 = { coe := fun (f : M₁ →ₚ M₂) => f.toFun }

def LO.Modal.Kripke.Model.PseudoEpimorphism.id {M : LO.Modal.Kripke.Model} : M →ₚ M

Equations

• LO.Modal.Kripke.Model.PseudoEpimorphism.id = { toFun := id, forth := ⋯, back := ⋯, atomic := ⋯ }

def LO.Modal.Kripke.Model.PseudoEpimorphism.mkAtomic {M₁ M₂ : LO.Modal.Kripke.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 := ⋯ }

def LO.Modal.Kripke.Model.PseudoEpimorphism.comp {M₁ M₂ M₃ : LO.Modal.Kripke.Model} (f : M₁ →ₚ M₂) (g : M₂ →ₚ M₃) : M₁ →ₚ M₃

Equations

• f.comp g = LO.Modal.Kripke.Model.PseudoEpimorphism.mkAtomic (f.comp g.toPseudoEpimorphism) ⋯

def LO.Modal.Kripke.Model.PseudoEpimorphism.bisimulation {M₁ M₂ : LO.Modal.Kripke.Model} (f : M₁ →ₚ M₂) : M₁ ⇄ M₂

Equations

• f.bisimulation = { toRel := Function.graph f.toFun, atomic := ⋯, forth := ⋯, back := ⋯ }

theorem LO.Modal.Kripke.Model.PseudoEpimorphism.modal_equivalence {M₁ M₂ : LO.Modal.Kripke.Model} (f : M₁ →ₚ M₂) (w : M₁.World) : w ↭ f.toFun w

theorem LO.Modal.Kripke.iff_formula_valid_on_frame_surjective_morphism {F₁ F₂ : LO.Modal.Kripke.Frame} {φ : LO.Modal.Formula ℕ} (f : F₁ →ₚ F₂) (f_surjective : Function.Surjective f.toFun) : F₁ ⊧ φ → F₂ ⊧ φ

theorem LO.Modal.Kripke.iff_theory_valid_on_frame_surjective_morphism {F₁ F₂ : LO.Modal.Kripke.Frame} {T : Set (LO.Modal.Formula ℕ)} (f : F₁ →ₚ F₂) (f_surjective : Function.Surjective f.toFun) : F₁ ⊧* T → F₂ ⊧* T

def LO.Modal.Kripke.Frame.isRooted (F : LO.Modal.Kripke.Frame) (r : F.World) : Prop

Equations

• F.isRooted r = ∀ (w : F.World), w ≠ r → r ≺ w

structure LO.Modal.Kripke.RootedFrameextends LO.Modal.Kripke.Frame : Type 1

• World : Type
• Rel : Rel self.World self.World
• world_nonempty : Nonempty self.World
• root : self.World
• root_rooted : self.isRooted self.root
• default : self.World

def LO.Modal.Kripke.Frame.PointGenerated (F : LO.Modal.Kripke.Frame) (r : F.World) : LO.Modal.Kripke.RootedFrame

Equations

• F↾r = { toFrame := LO.Modal.Kripke.Frame.mk ↑{w : F.World | w = r ∨ r ≺ w} fun (x y : ↑{w : F.World | w = r ∨ r ≺ w}) => ↑x ≺ ↑y, root := ⟨r, ⋯⟩, root_rooted := ⋯, default := ⟨r, ⋯⟩ }

def LO.Modal.Kripke.«term_↾_» : Lean.TrailingParserDescr

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))

theorem LO.Modal.Kripke.Frame.PointGenerated.rel_transitive {F : LO.Modal.Kripke.Frame} {r : F.World} (F_trans : Transitive F.Rel) : Transitive (F↾r).Rel

theorem LO.Modal.Kripke.Frame.PointGenerated.rel_irreflexive {F : LO.Modal.Kripke.Frame} {r : F.World} (F_irrefl : Irreflexive F.Rel) : Irreflexive (F↾r).Rel

theorem LO.Modal.Kripke.Frame.PointGenerated.rel_universal {F : LO.Modal.Kripke.Frame} {r : F.World} (F_refl : Reflexive F.Rel) (F_eucl : Euclidean F.Rel) : Universal (F↾r).Rel

instance LO.Modal.Kripke.Frame.PointGenerated.instFiniteWorld {F : LO.Modal.Kripke.Frame} {r : F.World} [Finite F.World] : Finite (F↾r).World

Equations

• ⋯ = ⋯

instance LO.Modal.Kripke.Frame.PointGenerated.instDecidableEqWorld {F : LO.Modal.Kripke.Frame} {r : F.World} [DecidableEq F.World] : DecidableEq (F↾r).World

Equations

• LO.Modal.Kripke.Frame.PointGenerated.instDecidableEqWorld = Subtype.instDecidableEq

structure LO.Modal.Kripke.RootedModelextends LO.Modal.Kripke.Model, LO.Modal.Kripke.RootedFrame : Type 1

• World : Type
• Rel : Rel self.World self.World
• world_nonempty : Nonempty self.World
• Val : LO.Modal.Kripke.Valuation self.toFrame
• root : self.World
• root_rooted : self.isRooted self.root
• default : self.World

def LO.Modal.Kripke.Model.PointGenerated (M : LO.Modal.Kripke.Model) (r : M.World) : LO.Modal.Kripke.RootedModel

Equations

• M↾r = { toFrame := (M.toFrame↾r).toFrame, Val := fun (w : (M.toFrame↾r).World) (a : ℕ) => M.Val (↑w) a, root := (M.toFrame↾r).root, root_rooted := ⋯, default := (M.toFrame↾r).root }

def LO.Modal.Kripke.«term_↾__1» : Lean.TrailingParserDescr

Equations

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

def LO.Modal.Kripke.Model.PointGenerated.bisimulation_of_trans {M : LO.Modal.Kripke.Model} (M_trans : Transitive M.Rel) (r : M.World) : (M↾r).toModel ⇄ M

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 := ⋯ }

theorem LO.Modal.Kripke.Model.PointGenerated.modal_equivalent_at_root {M : LO.Modal.Kripke.Model} (M_trans : Transitive M.Rel) (r : M.World) : ⟨r, ⋯⟩ ↭ r

structure LO.Modal.Kripke.Frame.GeneratedSub (F₁ F₂ : LO.Modal.Kripke.Frame) extends F₁ →ₚ F₂ : Type

• toFun : F₁.World → F₂.World
• forth : ∀ {x y : F₁.World}, x ≺ y → self.toFun x ≺ self.toFun y
• back : ∀ {w : F₁.World} {v : F₂.World}, self.toFun w ≺ v → ∃ (u : F₁.World), self.toFun u = v ∧ w ≺ u
• monic : Function.Injective self.toFun

def LO.Modal.Kripke.«term_⊆ₚ_» : Lean.TrailingParserDescr

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))

@[reducible, inline]

abbrev LO.Modal.Kripke.IrreflexiveFrameClass : LO.Modal.Kripke.FrameClass

Equations

• LO.Modal.Kripke.IrreflexiveFrameClass = {F : LO.Modal.Kripke.Frame | Irreflexive F.Rel}

theorem LO.Modal.Kripke.undefinable_irreflexive : ¬∃ (Ax : LO.Modal.Theory ℕ), LO.Modal.Kripke.IrreflexiveFrameClass.DefinedBy Ax