---

Step * 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 
⊢ ∃k:ℕn + 1. ∀i:ℕn + 1. f i ≤loc f k 
BY
{ (Decide ⌈f n ≤loc f k ⌉⋅ THENA 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 
⊢ ∃k:ℕn + 1. ∀i:ℕn + 1. f i ≤loc f k 

2
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 
⊢ ∃k:ℕn + 1. ∀i:ℕn + 1. f i ≤loc f k 

---

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 
\mvdash{}  \mexists{}k:\mBbbN{}n  +  1.  \mforall{}i:\mBbbN{}n  +  1.  f  i  \mleq{}loc  f  k 


By

(Decide  \mkleeneopen{}f  n  \mleq{}loc  f  k  \mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index