---

Step * 1 1 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);L)
BY
{ ((Assert ⌈l-ordered(E;x,y.(x <loc y);filter(P;[e1, e2]))⌉⋅ THENM (FLemma `iseg-l-ordered` [-5;-1] THEN Auto))
   THEN (BLemma `l-ordered-filter2` THEN Auto)
   THEN BLemma `es-interval-ordered`
   THEN Auto) }

---

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);L)


By

((Assert  \mkleeneopen{}l-ordered(E;x,y.(x  <loc  y);filter(P;[e1,  e2]))\mkleeneclose{}\mcdot{}
  THENM  (FLemma  `iseg-l-ordered`  [-5;-1]  THEN  Auto)
  )
  THEN  (BLemma  `l-ordered-filter2`  THEN  Auto)
  THEN  BLemma  `es-interval-ordered`
  THEN  Auto)

---

Home Index