@[reducible, inline]

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

Equations

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

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

Equations

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

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 {α : Type u_1} {M₁ : LO.Kripke.Model α} {M₂ : LO.Kripke.Model α} {x₁ : M₁.World} {x₂ : M₂.World} (Bi : M₁ ⇄ M₂) (bisx : Bi.toRel x₁ x₂) : x₁ ↭ x₂

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

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

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

theorem LO.Modal.Kripke.undefinable_irreflexive {α : Type u_1} : ¬∃ (Λ : LO.Modal.Hilbert α), ∀ (F : LO.Kripke.Frame), F ∈ 𝔽(Λ) ↔ F ∈ LO.Kripke.IrreflexiveFrameClass

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