---

Step * 1 3 of Lemma iseg-filter-es-interval


1. es : EO
2. L : E List
3. e1 : E
4. e2 : E
5. P : {x:E| (x ∈ [e1, e2])}  ─→ 𝔹
6. L ≤ filter(P;[e1, e2])
7. ¬↑null(L)
8. (last(L) ∈ L)
9. (last(L) ∈ [e1, e2])
10. (L = filter(P;[e1, last(L)]) ∈ (E List)) ⇒ (∀x:E. ((x ∈ L) ⇐⇒ (x ∈ filter(P;[e1, last(L)]))))
11. (L = filter(P;[e1, last(L)]) ∈ (E List)) ⇐ ∀x:E. ((x ∈ L) ⇐⇒ (x ∈ filter(P;[e1, last(L)])))
12. x : E@i
13. (x ∈ L)@i
⊢ (x ∈ filter(P;[e1, last(L)]))
BY
{ ((FLemma `iseg_member` [-8;-1] THENA Auto) THEN RW ListC 0 THEN Auto) }

1
.....wf..... 
1. es : EO
2. L : E List
3. e1 : E
4. e2 : E
5. P : {x:E| (x ∈ [e1, e2])}  ─→ 𝔹
6. L ≤ filter(P;[e1, e2])
7. ¬↑null(L)
8. (last(L) ∈ L)
9. (last(L) ∈ [e1, e2])
10. (L = filter(P;[e1, last(L)]) ∈ (E List)) ⇒ (∀x:E. ((x ∈ L) ⇐⇒ (x ∈ filter(P;[e1, last(L)]))))
11. (L = filter(P;[e1, last(L)]) ∈ (E List)) ⇐ ∀x:E. ((x ∈ L) ⇐⇒ (x ∈ filter(P;[e1, last(L)])))
12. x : E@i
13. (x ∈ L)@i
14. (x ∈ filter(P;[e1, e2]))
⊢ P ∈ {x:E| (x ∈ [e1, last(L)])}  ─→ 𝔹

2
1. es : EO
2. L : E List
3. e1 : E
4. e2 : E
5. P : {x:E| (x ∈ [e1, e2])}  ─→ 𝔹
6. L ≤ filter(P;[e1, e2])
7. ¬↑null(L)
8. (last(L) ∈ L)
9. (last(L) ∈ [e1, e2])
10. (L = filter(P;[e1, last(L)]) ∈ (E List)) ⇒ (∀x:E. ((x ∈ L) ⇐⇒ (x ∈ filter(P;[e1, last(L)]))))
11. (L = filter(P;[e1, last(L)]) ∈ (E List)) ⇐ ∀x:E. ((x ∈ L) ⇐⇒ (x ∈ filter(P;[e1, last(L)])))
12. x : E@i
13. (x ∈ L)@i
14. (x ∈ filter(P;[e1, e2]))
⊢ (x ∈ [e1, last(L)])

3
1. es : EO
2. L : E List
3. e1 : E
4. e2 : E
5. P : {x:E| (x ∈ [e1, e2])}  ─→ 𝔹
6. L ≤ filter(P;[e1, e2])
7. ¬↑null(L)
8. (last(L) ∈ L)
9. (last(L) ∈ [e1, e2])
10. (L = filter(P;[e1, last(L)]) ∈ (E List)) ⇒ (∀x:E. ((x ∈ L) ⇐⇒ (x ∈ filter(P;[e1, last(L)]))))
11. (L = filter(P;[e1, last(L)]) ∈ (E List)) ⇐ ∀x:E. ((x ∈ L) ⇐⇒ (x ∈ filter(P;[e1, last(L)])))
12. x : E@i
13. (x ∈ L)@i
14. (x ∈ filter(P;[e1, e2]))
15. (x ∈ [e1, last(L)])
⊢ ↑(P x)

---

Latex:



1.  es  :  EO
2.  L  :  E  List
3.  e1  :  E
4.  e2  :  E
5.  P  :  \{x:E|  (x  \mmember{}  [e1,  e2])\}    {}\mrightarrow{}  \mBbbB{}
6.  L  \mleq{}  filter(P;[e1,  e2])
7.  \mneg{}\muparrow{}null(L)
8.  (last(L)  \mmember{}  L)
9.  (last(L)  \mmember{}  [e1,  e2])
10.  (L  =  filter(P;[e1,  last(L)]))  {}\mRightarrow{}  (\mforall{}x:E.  ((x  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  filter(P;[e1,  last(L)]))))
11.  (L  =  filter(P;[e1,  last(L)]))  \mLeftarrow{}{}  \mforall{}x:E.  ((x  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  filter(P;[e1,  last(L)])))
12.  x  :  E@i
13.  (x  \mmember{}  L)@i
\mvdash{}  (x  \mmember{}  filter(P;[e1,  last(L)]))


By

((FLemma  `iseg\_member`  [-8;-1]  THENA  Auto)  THEN  RW  ListC  0  THEN  Auto)

---

Home Index