---

Step * of Lemma local-pred-class_wf

∀[Info:Type]. ∀[P:es:EO+(Info) ⟶ E ⟶ 𝔹].
  (local-pred-class(P) ∈ EClass({e':E| 
                                 (e' <loc e)
                                 ∧ (↑(P es e'))
                                 ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(P es e''))))} ))
BY
{ (Unfolds ``eclass local-pred-class`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[P:es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbB{}].
    (local-pred-class(P)  \mmember{}  EClass(\{e':E| 
                                                                  (e'  <loc  e)
                                                                  \mwedge{}  (\muparrow{}(P  es  e'))
                                                                  \mwedge{}  (\mforall{}e'':E.  ((e'  <loc  e'')  {}\mRightarrow{}  (e''  <loc  e)  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  es  e''))))\}  ))


By

---

Latex:
(Unfolds  ``eclass  local-pred-class``  0  THEN  Auto)

---

Home Index