---

Step * of Lemma es-is-le-interface

∀[Info:Type]. ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E.  (↑e ∈b le(X) ⇐⇒ ∃e':E. (e' ≤loc e  ∧ (↑e' ∈b X)))
BY
{ ((UnivCD THENA Auto)
   THEN ((InstLemma `es-local-le-pred-property` [⌜Info⌝;⌜λes,e. e ∈b X⌝;⌜es⌝;⌜e⌝])⋅ THENA Auto)
   THEN (Reduce (-1))
   THEN (Fold `es-le-interface` (-1))
   THEN D -1
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  le(X)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e':E.  (e'  \mleq{}loc  e    \mwedge{}  (\muparrow{}e'  \mmember{}\msubb{}  X)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  ((InstLemma  `es-local-le-pred-property`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}\mlambda{}es,e.  e  \mmember{}\msubb{}  X\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  (Reduce  (-1))
  THEN  (Fold  `es-le-interface`  (-1))
  THEN  D  -1
  THEN  Trivial)

---

Home Index