Documentation

Foundation.Modal.Kripke.Preservation

  • 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₁
Instances For
    instance LO.Modal.Kripke.instCoeFunBisimulationForallWorldForallProp {M₁ M₂ : Model} :
    CoeFun (M₁ M₂) fun (x : M₁ M₂) => M₁.WorldM₂.WorldProp
    Equations
    def LO.Modal.Kripke.ModalEquivalent {M₁ M₂ : Model} (w₁ : M₁.World) (w₂ : M₂.World) :
    Equations
    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₂
      • toFun : F₁.WorldF₂.World
      • forth {x y : F₁.World} : x yself.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
      Instances For
        instance LO.Modal.Kripke.instCoeFunPseudoEpimorphismForallWorld {F₁ F₂ : Frame} :
        CoeFun (F₁ →ₚ F₂) fun (x : F₁ →ₚ F₂) => F₁.WorldF₂.World
        Equations
        Equations
        Instances For
          def LO.Modal.Kripke.Frame.PseudoEpimorphism.TransitiveClosure {F₁ F₂ : Frame} (f : F₁ →ₚ F₂) (F₂_trans : Transitive F₂.Rel) :
          F₁^+ →ₚ F₂
          Equations
          • f.TransitiveClosure F₂_trans = { toFun := f.toFun, forth := , back := }
          Instances For
            def LO.Modal.Kripke.Frame.PseudoEpimorphism.comp {F₁ F₂ F₃ : Frame} (f : F₁ →ₚ F₂) (g : F₂ →ₚ F₃) :
            F₁ →ₚ F₃
            Equations
            • f.comp g = { toFun := g.toFun f.toFun, forth := , back := }
            Instances For
              structure LO.Modal.Kripke.Model.PseudoEpimorphism (M₁ M₂ : Model) extends M₁.toFrame →ₚ M₂.toFrame :
              • toFun : M₁.WorldM₂.World
              • forth {x y : M₁.World} : x yself.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
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  instance LO.Modal.Kripke.instCoeFunPseudoEpimorphismForallWorld_1 {M₁ M₂ : Model} :
                  CoeFun (M₁ →ₚ M₂) fun (x : M₁ →ₚ M₂) => M₁.WorldM₂.World
                  Equations
                  Equations
                  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
                    Instances For
                      def LO.Modal.Kripke.Model.PseudoEpimorphism.comp {M₁ M₂ M₃ : Model} (f : M₁ →ₚ M₂) (g : M₂ →ₚ M₃) :
                      M₁ →ₚ M₃
                      Equations
                      Instances For
                        def LO.Modal.Kripke.Model.PseudoEpimorphism.bisimulation {M₁ M₂ : Model} (f : M₁ →ₚ M₂) :
                        M₁ M₂
                        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) :
                          F₁ φF₂ φ
                          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) :
                          F₁ ⊧* TF₂ ⊧* T
                          def LO.Modal.Kripke.Frame.isRooted (F : Frame) (r : F.World) :
                          Equations
                          • F.isRooted r = ∀ (w : F.World), w rr w
                          Instances For
                            Instances For
                              Equations
                              Instances For
                                theorem LO.Modal.Kripke.Frame.PointGenerated.rel_transitive {F : Frame} {r : F.World} (F_trans : Transitive F.Rel) :
                                Transitive (Fr).Rel
                                theorem LO.Modal.Kripke.Frame.PointGenerated.rel_irreflexive {F : Frame} {r : F.World} (F_irrefl : Irreflexive F.Rel) :
                                theorem LO.Modal.Kripke.Frame.PointGenerated.rel_universal {F : Frame} {r : F.World} (F_refl : Reflexive F.Rel) (F_eucl : Euclidean F.Rel) :
                                Universal (Fr).Rel
                                instance LO.Modal.Kripke.Frame.PointGenerated.instFiniteWorld {F : Frame} {r : F.World} [Finite F.World] :
                                Finite (Fr).World
                                Instances For
                                  Equations
                                  • Mr = { toFrame := (M.toFramer).toFrame, Val := fun (w : (M.toFramer).World) (a : ) => M.Val (↑w) a, root := (M.toFramer).root, root_rooted := , default := (M.toFramer).root }
                                  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) :
                                      (Mr).toModel M
                                      Equations
                                      Instances For
                                        theorem LO.Modal.Kripke.Model.PointGenerated.modal_equivalent_at_root {M : Model} (M_trans : Transitive M.Rel) (r : M.World) :
                                        r, r
                                        structure LO.Modal.Kripke.Frame.GeneratedSub (F₁ F₂ : Frame) extends F₁ →ₚ F₂ :
                                        • toFun : F₁.WorldF₂.World
                                        • forth {x y : F₁.World} : x yself.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
                                        Instances For