structure LO.Modal.Standard.Kripke.Model.Bisimulation {α : Type u_1} (M₁ : LO.Modal.Standard.Kripke.Model α) (M₂ : LO.Modal.Standard.Kripke.Model α) : Type (max u_2 u_3)

• toRel : Rel M₁.World M₂.World
• atomic : ∀ {x₁ : M₁.World} {x₂ : M₂.World} {a : α}, self.toRel x₁ x₂ → (M₁.Valuation x₁ a ↔ M₂.Valuation x₂ a)
• forth : ∀ {x₁ y₁ : M₁.World} {x₂ : M₂.World}, self.toRel x₁ x₂ → LO.Modal.Standard.Kripke.Frame.Rel' x₁ y₁ → ∃ (y₂ : M₂.World), self.toRel y₁ y₂ ∧ LO.Modal.Standard.Kripke.Frame.Rel' x₂ y₂
• back : ∀ {x₁ : M₁.World} {x₂ y₂ : M₂.World}, self.toRel x₁ x₂ → LO.Modal.Standard.Kripke.Frame.Rel' x₂ y₂ → ∃ (y₁ : M₁.World), self.toRel y₁ y₂ ∧ LO.Modal.Standard.Kripke.Frame.Rel' x₁ y₁

theorem LO.Modal.Standard.Kripke.Model.Bisimulation.atomic {α : Type u_1} {M₁ : LO.Modal.Standard.Kripke.Model α} {M₂ : LO.Modal.Standard.Kripke.Model α} (self : M₁ ⇄ M₂) {x₁ : M₁.World} {x₂ : M₂.World} {a : α} : self.toRel x₁ x₂ → (M₁.Valuation x₁ a ↔ M₂.Valuation x₂ a)

theorem LO.Modal.Standard.Kripke.Model.Bisimulation.forth {α : Type u_1} {M₁ : LO.Modal.Standard.Kripke.Model α} {M₂ : LO.Modal.Standard.Kripke.Model α} (self : M₁ ⇄ M₂) {x₁ : M₁.World} {y₁ : M₁.World} {x₂ : M₂.World} : self.toRel x₁ x₂ → LO.Modal.Standard.Kripke.Frame.Rel' x₁ y₁ → ∃ (y₂ : M₂.World), self.toRel y₁ y₂ ∧ LO.Modal.Standard.Kripke.Frame.Rel' x₂ y₂

theorem LO.Modal.Standard.Kripke.Model.Bisimulation.back {α : Type u_1} {M₁ : LO.Modal.Standard.Kripke.Model α} {M₂ : LO.Modal.Standard.Kripke.Model α} (self : M₁ ⇄ M₂) {x₁ : M₁.World} {x₂ : M₂.World} {y₂ : M₂.World} : self.toRel x₁ x₂ → LO.Modal.Standard.Kripke.Frame.Rel' x₂ y₂ → ∃ (y₁ : M₁.World), self.toRel y₁ y₂ ∧ LO.Modal.Standard.Kripke.Frame.Rel' x₁ y₁

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

Equations

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

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

Equations

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

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

Equations

• (w₁ ↭ w₂) = ∀ {p : LO.Modal.Standard.Formula α}, w₁ ⊧ p ↔ w₂ ⊧ p

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

Equations

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

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

structure LO.Modal.Standard.Kripke.Frame.PseudoEpimorphism (F₁ : LO.Modal.Standard.Kripke.Frame) (F₂ : LO.Modal.Standard.Kripke.Frame) : Type (max u_1 u_2)

As known as p-morphism.

• toFun : F₁.World → F₂.World
• forth : ∀ {x y : F₁.World}, LO.Modal.Standard.Kripke.Frame.Rel' x y → LO.Modal.Standard.Kripke.Frame.Rel' (self.toFun x) (self.toFun y)
• back : ∀ {w : F₁.World} {v : F₂.World}, LO.Modal.Standard.Kripke.Frame.Rel' (self.toFun w) v → ∃ (u : F₁.World), self.toFun u = v ∧ LO.Modal.Standard.Kripke.Frame.Rel' w u

theorem LO.Modal.Standard.Kripke.Frame.PseudoEpimorphism.forth {F₁ : LO.Modal.Standard.Kripke.Frame} {F₂ : LO.Modal.Standard.Kripke.Frame} (self : F₁ →ₚ F₂) {x : F₁.World} {y : F₁.World} : LO.Modal.Standard.Kripke.Frame.Rel' x y → LO.Modal.Standard.Kripke.Frame.Rel' (self.toFun x) (self.toFun y)

theorem LO.Modal.Standard.Kripke.Frame.PseudoEpimorphism.back {F₁ : LO.Modal.Standard.Kripke.Frame} {F₂ : LO.Modal.Standard.Kripke.Frame} (self : F₁ →ₚ F₂) {w : F₁.World} {v : F₂.World} : LO.Modal.Standard.Kripke.Frame.Rel' (self.toFun w) v → ∃ (u : F₁.World), self.toFun u = v ∧ LO.Modal.Standard.Kripke.Frame.Rel' w u

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

structure LO.Modal.Standard.Kripke.Model.PseudoEpimorphism {α : Type u_1} (M₁ : LO.Modal.Standard.Kripke.Model α) (M₂ : LO.Modal.Standard.Kripke.Model α) extends LO.Modal.Standard.Kripke.Frame.PseudoEpimorphism : Type (max u_2 u_3)

• toFun : M₁.Frame.World → M₂.Frame.World
• forth : ∀ {x y : M₁.Frame.World}, LO.Modal.Standard.Kripke.Frame.Rel' x y → LO.Modal.Standard.Kripke.Frame.Rel' (self.toFun x) (self.toFun y)
• back : ∀ {w : M₁.Frame.World} {v : M₂.Frame.World}, LO.Modal.Standard.Kripke.Frame.Rel' (self.toFun w) v → ∃ (u : M₁.Frame.World), self.toFun u = v ∧ LO.Modal.Standard.Kripke.Frame.Rel' w u
• atomic : ∀ {w : M₁.World} {a : α}, M₁.Valuation w a ↔ M₂.Valuation (self.toFun w) a

theorem LO.Modal.Standard.Kripke.Model.PseudoEpimorphism.atomic {α : Type u_1} {M₁ : LO.Modal.Standard.Kripke.Model α} {M₂ : LO.Modal.Standard.Kripke.Model α} (self : M₁ →ₚ M₂) {w : M₁.World} {a : α} : M₁.Valuation w a ↔ M₂.Valuation (self.toFun w) a

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

Equations

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

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

Equations

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

def LO.Modal.Standard.Kripke.Model.PseudoEpimorphism.toFramePseudoEpimorphism {α : Type u_1} {M₁ : LO.Modal.Standard.Kripke.Model α} {M₂ : LO.Modal.Standard.Kripke.Model α} (f : M₁ →ₚ M₂) : M₁.Frame →ₚ M₂.Frame

Equations

• f.toFramePseudoEpimorphism = { toFun := f.toFun, forth := ⋯, back := ⋯ }

def LO.Modal.Standard.Kripke.Model.PseudoEpimorphism.id {α : Type u_1} {M : LO.Modal.Standard.Kripke.Model α} : M →ₚ M

Equations

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

def LO.Modal.Standard.Kripke.Model.PseudoEpimorphism.mkAtomic {α : Type u_1} {M₁ : LO.Modal.Standard.Kripke.Model α} {M₂ : LO.Modal.Standard.Kripke.Model α} (f : M₁.Frame →ₚ M₂.Frame) (atomic : ∀ {w : M₁.Frame.World} {a : α}, M₁.Valuation w a ↔ M₂.Valuation (f.toFun w) a) : M₁ →ₚ M₂

Equations

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

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

Equations

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

def LO.Modal.Standard.Kripke.Model.PseudoEpimorphism.Bisimulation {α : Type u_1} {M₁ : LO.Modal.Standard.Kripke.Model α} {M₂ : LO.Modal.Standard.Kripke.Model α} (f : M₁ →ₚ M₂) : M₁ ⇄ M₂

Equations

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

theorem LO.Modal.Standard.Kripke.modal_equivalence_of_modal_morphism {α : Type u_1} {M₁ : LO.Modal.Standard.Kripke.Model α} {M₂ : LO.Modal.Standard.Kripke.Model α} (f : M₁ →ₚ M₂) (w : M₁.World) : w ↭ f.toFun w

theorem LO.Modal.Standard.Kripke.iff_formula_valid_on_frame_surjective_morphism {α : Type u_3} {F₁ : LO.Modal.Standard.Kripke.Frame} {F₂ : LO.Modal.Standard.Kripke.Frame} {p : LO.Modal.Standard.Formula α} (f : F₁ →ₚ F₂) (f_surjective : Function.Surjective f.toFun) : F₁.alt ⊧ p → F₂.alt ⊧ p

theorem LO.Modal.Standard.Kripke.iff_theory_valid_on_frame_surjective_morphism {F₁ : LO.Modal.Standard.Kripke.Frame} {F₂ : LO.Modal.Standard.Kripke.Frame} : ∀ {α : Type u_1} {T : Set (LO.Modal.Standard.Formula α)} (f : F₁ →ₚ F₂), Function.Surjective f.toFun → F₁.alt ⊧* T → F₂.alt ⊧* T

@[reducible, inline]

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

Equations

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

theorem LO.Modal.Standard.Kripke.undefinable_irreflexive {α : Type u_1} : ¬∃ (Ax : LO.Modal.Standard.AxiomSet α), Ax.DefinesKripkeFrameClass LO.Modal.Standard.Kripke.IrreflexiveFrameClass

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

Equations

• F.isRooted r = ∀ (w : F.World), w ≠ r → LO.Modal.Standard.Kripke.Frame.Rel' r w

structure LO.Modal.Standard.Kripke.RootedFrameextends LO.Modal.Standard.Kripke.Frame : Type (u_1 + 1)

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

theorem LO.Modal.Standard.Kripke.RootedFrame.root_rooted (self : LO.Modal.Standard.Kripke.RootedFrame) : self.isRooted self.root

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

Equations

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

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

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

theorem LO.Modal.Standard.Kripke.Frame.PointGenerated.rooted {F : LO.Modal.Standard.Kripke.Frame} {r : F.World} : (F.PointGenerated r).isRooted ⟨r, ⋯⟩

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

Equations

• ⋯ = ⋯

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Standard.Kripke.Frame.PointGenerated' (F : LO.Modal.Standard.Kripke.Frame) (r : F.World) : LO.Modal.Standard.Kripke.RootedFrame

Equations

• F↾r = { toFrame := LO.Modal.Standard.Kripke.Frame.mk (F.PointGenerated r).World (F.PointGenerated r).Rel, root := ⟨r, ⋯⟩, root_rooted := ⋯, default := ⟨r, ⋯⟩ }

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

Equations

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

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

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

def LO.Modal.Standard.Kripke.Model.PointGenerated {α : Type u_1} (M : LO.Modal.Standard.Kripke.Model α) (r : M.World) : LO.Modal.Standard.Kripke.Model α

Equations

• M↾r = { Frame := (M.Frame↾r).toFrame, Valuation := fun (w : (M.Frame↾r).World) (a : α) => M.Valuation (↑w) a }

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

Equations

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

def LO.Modal.Standard.Kripke.Model.PointGenerated.Bisimulation {α : Type u_1} (M : LO.Modal.Standard.Kripke.Model α) (M_trans : Transitive M.Frame.Rel) (r : M.World) : (M↾r) ⇄ M

Equations

• LO.Modal.Standard.Kripke.Model.PointGenerated.Bisimulation M M_trans r = { toRel := fun (x : (M↾r).World) (y : M.World) => ↑x = y, atomic := ⋯, forth := ⋯, back := ⋯ }

theorem LO.Modal.Standard.Kripke.Model.PointGenerated.Bisimulation.rooted : ∀ {α : Type u_1} {M : LO.Modal.Standard.Kripke.Model α} {r : M.World} (M_trans : autoParam (Transitive M.Frame.Rel) _auto✝), (LO.Modal.Standard.Kripke.Model.PointGenerated.Bisimulation M M_trans r).toRel ⟨r, ⋯⟩ r

theorem LO.Modal.Standard.Kripke.Model.PointGenerated.modal_equivalent_to_root {α : Type u_1} (M : LO.Modal.Standard.Kripke.Model α) (M_trans : Transitive M.Frame.Rel) (r : M.World) : ⟨r, ⋯⟩ ↭ r

structure LO.Modal.Standard.Kripke.Frame.GeneratedSub (F₁ : LO.Modal.Standard.Kripke.Frame) (F₂ : LO.Modal.Standard.Kripke.Frame) extends LO.Modal.Standard.Kripke.Frame.PseudoEpimorphism : Type (max u_1 u_2)

• toFun : F₁.World → F₂.World
• forth : ∀ {x y : F₁.World}, LO.Modal.Standard.Kripke.Frame.Rel' x y → LO.Modal.Standard.Kripke.Frame.Rel' (self.toFun x) (self.toFun y)
• back : ∀ {w : F₁.World} {v : F₂.World}, LO.Modal.Standard.Kripke.Frame.Rel' (self.toFun w) v → ∃ (u : F₁.World), self.toFun u = v ∧ LO.Modal.Standard.Kripke.Frame.Rel' w u
• monic : Function.Injective self.toFun

theorem LO.Modal.Standard.Kripke.Frame.GeneratedSub.monic {F₁ : LO.Modal.Standard.Kripke.Frame} {F₂ : LO.Modal.Standard.Kripke.Frame} (self : F₁ ⊆ₚ F₂) : Function.Injective self.toFun

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

Equations

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

def LO.Modal.Standard.Kripke.Frame.successors {F : LO.Modal.Standard.Kripke.Frame} (x : F.World) : Type u_1

Equations

• LO.Modal.Standard.Kripke.Frame.successors x = { w : F.World // LO.Modal.Standard.Kripke.Frame.RelReflTransGen x w }

def LO.Modal.Standard.Kripke.Frame.«term_↑*» : Lean.TrailingParserDescr

Equations

• LO.Modal.Standard.Kripke.Frame.«term_↑*» = Lean.ParserDescr.trailingNode `LO.Modal.Standard.Kripke.Frame.term_↑* 100 100 (Lean.ParserDescr.symbol "↑*")

def LO.Modal.Standard.Kripke.Frame.immediate_successors {F : LO.Modal.Standard.Kripke.Frame} (x : F.World) : Type u_1

Equations

• LO.Modal.Standard.Kripke.Frame.immediate_successors x = { w : F.World // LO.Modal.Standard.Kripke.Frame.Rel' x w }

def LO.Modal.Standard.Kripke.Frame.«term_↑¹» : Lean.TrailingParserDescr

Equations

• LO.Modal.Standard.Kripke.Frame.«term_↑¹» = Lean.ParserDescr.trailingNode `LO.Modal.Standard.Kripke.Frame.term_↑¹ 100 100 (Lean.ParserDescr.symbol "↑¹")

def LO.Modal.Standard.Kripke.Frame.proper_immediate_successors {F : LO.Modal.Standard.Kripke.Frame} (x : F.World) : Type u_1

Equations

• LO.Modal.Standard.Kripke.Frame.proper_immediate_successors x = { w : F.World // x ≠ w ∧ LO.Modal.Standard.Kripke.Frame.Rel' x w }

def LO.Modal.Standard.Kripke.Frame.«term_↑» : Lean.TrailingParserDescr

Equations

• LO.Modal.Standard.Kripke.Frame.«term_↑» = Lean.ParserDescr.trailingNode `LO.Modal.Standard.Kripke.Frame.term_↑ 100 100 (Lean.ParserDescr.symbol "↑")

def LO.Modal.Standard.Kripke.Frame.predeccsors {F : LO.Modal.Standard.Kripke.Frame} (x : F.World) : Type u_1

Equations

• LO.Modal.Standard.Kripke.Frame.predeccsors x = { w : F.World // LO.Modal.Standard.Kripke.Frame.RelReflTransGen w x }

def LO.Modal.Standard.Kripke.Frame.«term_↓*» : Lean.TrailingParserDescr

Equations

• LO.Modal.Standard.Kripke.Frame.«term_↓*» = Lean.ParserDescr.trailingNode `LO.Modal.Standard.Kripke.Frame.term_↓* 100 100 (Lean.ParserDescr.symbol "↓*")

def LO.Modal.Standard.Kripke.Frame.immediate_predeccsors {F : LO.Modal.Standard.Kripke.Frame} (x : F.World) : Type u_1

Equations

• LO.Modal.Standard.Kripke.Frame.immediate_predeccsors x = { w : F.World // LO.Modal.Standard.Kripke.Frame.Rel' w x }

def LO.Modal.Standard.Kripke.Frame.«term_↓¹» : Lean.TrailingParserDescr

Equations

• LO.Modal.Standard.Kripke.Frame.«term_↓¹» = Lean.ParserDescr.trailingNode `LO.Modal.Standard.Kripke.Frame.term_↓¹ 100 100 (Lean.ParserDescr.symbol "↓¹")

def LO.Modal.Standard.Kripke.Frame.proper_immediate_predeccsors {F : LO.Modal.Standard.Kripke.Frame} (x : F.World) : Type u_1

Equations

• x↓ = { w : F.World // w ≠ x ∧ LO.Modal.Standard.Kripke.Frame.Rel' w x }

def LO.Modal.Standard.Kripke.Frame.«term_↓» : Lean.TrailingParserDescr

Equations

• LO.Modal.Standard.Kripke.Frame.«term_↓» = Lean.ParserDescr.trailingNode `LO.Modal.Standard.Kripke.Frame.term_↓ 100 100 (Lean.ParserDescr.symbol "↓")