---

Step * 1 1 1 1 1 of Lemma prior-imax-class-lb2


1. Info : Type
2. es : EO+(Info)
3. e : E
4. n : ℕ
5. A : Type
6. f : A ─→ ℕ
7. Z : EClass(A)
8. ¬↑e ∈b Z
9. ↑e ∈b ((maximum f[x] ≥ 0 with x from Z))'
10. e' : E
11. (e' <loc e)
12. ↑e' ∈b (maximum f[x] ≥ 0 with x from Z)
13. ∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑e'' ∈b (maximum f[x] ≥ 0 with x from Z)))
14. ((maximum f[x] ≥ 0 with x from Z))'(e) = (maximum f[x] ≥ 0 with x from Z)(e') ∈ ℤ
15. ↑e' ∈b Z
16. ∀[e1:E(Z)]. f[Z(e1)] ≤ n supposing e1 ≤loc e' 
17. 0 ≤ n
18. e1 : E(Z)
19. e1 ≤loc e 
20. ¬e1 ≤loc e' 
⊢ e1 ≤loc e' 
BY
{ OnMaybeHyp 11 (\h. (InstHyp [⌈e1⌉] h⋅ THEN Auto THEN D (-1) THEN RWO "is-imax-class" 0 THEN Auto)) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  e  :  E
4.  n  :  \mBbbN{}
5.  A  :  Type
6.  f  :  A  {}\mrightarrow{}  \mBbbN{}
7.  Z  :  EClass(A)
8.  \mneg{}\muparrow{}e  \mmember{}\msubb{}  Z
9.  \muparrow{}e  \mmember{}\msubb{}  ((maximum  f[x]  \mgeq{}  0  with  x  from  Z))'
10.  e'  :  E
11.  (e'  <loc  e)
12.  \muparrow{}e'  \mmember{}\msubb{}  (maximum  f[x]  \mgeq{}  0  with  x  from  Z)
13.  \mforall{}e'':E.  ((e'  <loc  e'')  {}\mRightarrow{}  (e''  <loc  e)  {}\mRightarrow{}  (\mneg{}\muparrow{}e''  \mmember{}\msubb{}  (maximum  f[x]  \mgeq{}  0  with  x  from  Z)))
14.  ((maximum  f[x]  \mgeq{}  0  with  x  from  Z))'(e)  =  (maximum  f[x]  \mgeq{}  0  with  x  from  Z)(e')
15.  \muparrow{}e'  \mmember{}\msubb{}  Z
16.  \mforall{}[e1:E(Z)].  f[Z(e1)]  \mleq{}  n  supposing  e1  \mleq{}loc  e' 
17.  0  \mleq{}  n
18.  e1  :  E(Z)
19.  e1  \mleq{}loc  e 
20.  \mneg{}e1  \mleq{}loc  e' 
\mvdash{}  e1  \mleq{}loc  e' 


By

---

Latex:
OnMaybeHyp  11  (\mbackslash{}h.  (InstHyp  [\mkleeneopen{}e1\mkleeneclose{}]  h\mcdot{}  THEN  Auto  THEN  D  (-1)  THEN  RWO  "is-imax-class"  0  THEN  Auto))

---

Home Index