---

Step * 1 2 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])
⊢ l-ordered(E;x,y.(x <loc y);filter(P;[e1, last(L)]))
BY
{ ((BLemma `l-ordered-filter2` THEN Auto) THEN Try ((BLemma `es-interval-ordered` 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])
⊢ P ∈ {x:E| (x ∈ [e1, last(L)])}  ─→ 𝔹

---

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])
\mvdash{}  l-ordered(E;x,y.(x  <loc  y);filter(P;[e1,  last(L)]))


By

((BLemma  `l-ordered-filter2`  THEN  Auto)  THEN  Try  ((BLemma  `es-interval-ordered`  THEN  Auto)))

---

Home Index