---

Step * 1 of Lemma es-pplus-alle-between2


1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. [Q] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
5. [e1,e2]~([a,b].∀e∈[a,b].Q[e])+@i
6. e1 ≤loc e2 
⊢ ∀e∈[e1,e2].Q[e]
BY
{ ((D (-2)) THEN ExRepD THEN D 0 THEN Auto) }

1
1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. [Q] : {e:E| loc(e) = loc(e1) ∈ Id}  ─→ ℙ
5. m : ℕ+@i
6. f : ℕm ─→ {e:E| loc(e) = loc(e1) ∈ Id} @i
7. (f 0) = e1 ∈ E@i
8. f (m - 1) ≤loc e2 @i
9. ∀i:ℕm - 1. (f i <loc f (i + 1))@i
10. ∀i:ℕm - 1. ∀e∈[f i,pred(f (i + 1))].Q[e]@i
11. ∀e∈[f (m - 1),e2].Q[e]@i
12. e1 ≤loc e2 
13. e : E@i
14. e1 ≤loc e @i
15. e ≤loc e2 @i
⊢ Q[e]

---

Latex:



1.  es  :  EO@i'
2.  e1  :  E@i
3.  e2  :  \{e:E|  loc(e)  =  loc(e1)\}  @i
4.  [Q]  :  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}
5.  [e1,e2]\msim{}([a,b].\mforall{}e\mmember{}[a,b].Q[e])+@i
6.  e1  \mleq{}loc  e2 
\mvdash{}  \mforall{}e\mmember{}[e1,e2].Q[e]


By

((D  (-2))  THEN  ExRepD  THEN  D  0  THEN  Auto)

---

Home Index