---

Step * 1 1 of Lemma until-class-simple-comb


1. Info : Type
2. A : Type
3. X : EClass(A)
4. Y : EClass(Top)
5. es : EO+(Info)
6. e : E
7. e' : E
8. (e' <loc e)
9. v : Top
10. v ∈ Y(e')
11. ∀e''<e.(↓∃v:Top. v ∈ Y(e'')) ⇒ e'' ≤loc e' 
12. class-pred(Y;es;e) = (inl e') ∈ (E + Top)
13. ∀v:Top. (¬v ∈ Prior(Y)(e))
⊢ ↓∃e'<e.v ∈ Y(e') ∧ ∀e''<e.∀w:Top. (w ∈ Y(e'') ⇒ e'' ≤loc e' )
BY
{ ((D 0 THEN With ⌈e'⌉ (D 0)⋅ THEN Auto) THEN D 0 THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  X  :  EClass(A)
4.  Y  :  EClass(Top)
5.  es  :  EO+(Info)
6.  e  :  E
7.  e'  :  E
8.  (e'  <loc  e)
9.  v  :  Top
10.  v  \mmember{}  Y(e')
11.  \mforall{}e''<e.(\mdownarrow{}\mexists{}v:Top.  v  \mmember{}  Y(e''))  {}\mRightarrow{}  e''  \mleq{}loc  e' 
12.  class-pred(Y;es;e)  =  (inl  e')
13.  \mforall{}v:Top.  (\mneg{}v  \mmember{}  Prior(Y)(e))
\mvdash{}  \mdownarrow{}\mexists{}e'<e.v  \mmember{}  Y(e')  \mwedge{}  \mforall{}e''<e.\mforall{}w:Top.  (w  \mmember{}  Y(e'')  {}\mRightarrow{}  e''  \mleq{}loc  e'  )


By

---

Latex:
((D  0  THEN  With  \mkleeneopen{}e'\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)  THEN  D  0  THEN  Auto)

---

Home Index