---

Step * of Lemma iseg-filter-es-interval

∀[es:EO]. ∀[L:E List]. ∀[e1,e2:E]. ∀[P:{x:E| (x ∈ [e1, e2])}  ─→ 𝔹].
  (L = filter(P;[e1, last(L)]) ∈ (E List)) supposing ((¬↑null(L)) and L ≤ filter(P;[e1, e2]))
BY
{ (Auto
   THEN (Assert ⌈(last(L) ∈ L)⌉⋅ THENA Auto)
   THEN (Assert ⌈(last(L) ∈ [e1, e2])⌉⋅ THENA (FLemma `iseg_member` [-3;-1]⋅ THEN Auto))) }

1
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 = filter(P;[e1, last(L)]) ∈ (E List)

---

Latex:


\mforall{}[es:EO].  \mforall{}[L:E  List].  \mforall{}[e1,e2:E].  \mforall{}[P:\{x:E|  (x  \mmember{}  [e1,  e2])\}    {}\mrightarrow{}  \mBbbB{}].
    (L  =  filter(P;[e1,  last(L)]))  supposing  ((\mneg{}\muparrow{}null(L))  and  L  \mleq{}  filter(P;[e1,  e2]))


By

(Auto
  THEN  (Assert  \mkleeneopen{}(last(L)  \mmember{}  L)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(last(L)  \mmember{}  [e1,  e2])\mkleeneclose{}\mcdot{}  THENA  (FLemma  `iseg\_member`  [-3;-1]\mcdot{}  THEN  Auto)))

---

Home Index