---

Step * 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))'
⊢ uiff(((maximum f[x] ≥ 0 with x from Z))'(e) ≤ n;∀[e':E(Z)]. f[Z(e')] ≤ n supposing e' ≤loc e )
BY
{ ((FLemma `prior-val-val` [-1] THENA Auto) THEN ExRepD THEN (HypSubst' (-1) 0 THENA Auto)) }

1
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') ∈ ℤ
⊢ uiff((maximum f[x] ≥ 0 with x from Z)(e') ≤ n;∀[e':E(Z)]. f[Z(e')] ≤ n supposing e' ≤loc e )

---

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))'
\mvdash{}  uiff(((maximum  f[x]  \mgeq{}  0  with  x  from  Z))'(e)  \mleq{}  n;\mforall{}[e':E(Z)].  f[Z(e')]  \mleq{}  n  supposing  e'  \mleq{}loc  e  )


By

---

Latex:
((FLemma  `prior-val-val`  [-1]  THENA  Auto)  THEN  ExRepD  THEN  (HypSubst'  (-1)  0  THENA  Auto))

---

Home Index