---

Step * 1 5 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
⊢ P ∈ {x:E| (x ∈ [e1, last(L)])}  ─→ 𝔹
BY
{ (DoSubsume
   THEN Auto
   THEN SubtypeReasoning
   THEN Auto
   THEN (RW ListC (-1) THENA Auto)
   THEN (RW ListC 0 THEN Auto)
   THEN (RW ListC (-9) THEN Auto)
   THEN FLemma `es-le_transitivity` [-2;-9]
   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])
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
\mvdash{}  P  \mmember{}  \{x:E|  (x  \mmember{}  [e1,  last(L)])\}    {}\mrightarrow{}  \mBbbB{}


By

(DoSubsume
  THEN  Auto
  THEN  SubtypeReasoning
  THEN  Auto
  THEN  (RW  ListC  (-1)  THENA  Auto)
  THEN  (RW  ListC  0  THEN  Auto)
  THEN  (RW  ListC  (-9)  THEN  Auto)
  THEN  FLemma  `es-le\_transitivity`  [-2;-9]
  THEN  Auto)

---

Home Index