Documentation

Foundation.Modal.Kripke.GL.MDP

@[reducible, inline]
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Equations
    Instances For
      Equations
      Instances For
        theorem LO.Modal.GL.Kripke.MDPCounterexampleFrame.through_original_root {F₁ F₂ : Kripke.FiniteTransitiveTree} {x : (MDPCounterexampleFrame F₁ F₂).World} (h : (MDPCounterexampleFrame F₁ F₂).root x) :
        (x = (Sum.inr Sum.inl) F₁.root Sum.inr (Sum.inl F₁.root) x) x = (Sum.inr Sum.inr) F₂.root Sum.inr (Sum.inr F₂.root) x
        @[reducible, inline]
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For