---

Step * 2 1 2 2 1 of Lemma last-event-of-set


1. es : EO@i'
2. n : ℤ@i
3. 0 < n
4. ∀f:ℕn ─→ E. ∃k:ℕn. ∀i:ℕn. f i ≤loc f k  supposing ∀i,j:ℕn.  (loc(f i) = loc(f j) ∈ Id)@i
5. f : ℕn + 1 ─→ E@i
6. ∀i,j:ℕn + 1.  (loc(f i) = loc(f j) ∈ Id)
7. k : ℕn
8. ∀i:ℕn. f i ≤loc f k 
9. ¬f n ≤loc f k 
10. (f k <loc f n)
11. i : ℕn + 1@i
⊢ f i ≤loc f n 
BY
{ (Decide ⌈i = n ∈ ℤ⌉⋅ THEN Auto)⋅ }

1
1. es : EO@i'
2. n : ℤ@i
3. 0 < n
4. ∀f:ℕn ─→ E. ∃k:ℕn. ∀i:ℕn. f i ≤loc f k  supposing ∀i,j:ℕn.  (loc(f i) = loc(f j) ∈ Id)@i
5. f : ℕn + 1 ─→ E@i
6. ∀i,j:ℕn + 1.  (loc(f i) = loc(f j) ∈ Id)
7. k : ℕn
8. ∀i:ℕn. f i ≤loc f k 
9. ¬f n ≤loc f k 
10. (f k <loc f n)
11. i : ℕn + 1@i
12. ¬(i = n ∈ ℤ)
⊢ f i ≤loc f n 

---

Latex:



1.  es  :  EO@i'
2.  n  :  \mBbbZ{}@i
3.  0  <  n
4.  \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  E.  \mexists{}k:\mBbbN{}n.  \mforall{}i:\mBbbN{}n.  f  i  \mleq{}loc  f  k    supposing  \mforall{}i,j:\mBbbN{}n.    (loc(f  i)  =  loc(f  j))@i
5.  f  :  \mBbbN{}n  +  1  {}\mrightarrow{}  E@i
6.  \mforall{}i,j:\mBbbN{}n  +  1.    (loc(f  i)  =  loc(f  j))
7.  k  :  \mBbbN{}n
8.  \mforall{}i:\mBbbN{}n.  f  i  \mleq{}loc  f  k 
9.  \mneg{}f  n  \mleq{}loc  f  k 
10.  (f  k  <loc  f  n)
11.  i  :  \mBbbN{}n  +  1@i
\mvdash{}  f  i  \mleq{}loc  f  n 


By

(Decide  \mkleeneopen{}i  =  n\mkleeneclose{}\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index