---

Step * 1 of Lemma iseg_filter2


1. [T] : Type
2. L_2 : T List
3. P : {x:T| (x ∈ [])}  ⟶ 𝔹
4. L_2 ≤ filter(P;[])
⊢ ∃L_3:T List. (L_3 ≤ [] ∧ (L_2 = filter(P;L_3) ∈ (T List)))
BY
{ (InstConcl [⌜[]⌝]⋅ THEN Auto THEN Try ((SubsumeC  ⌜{x:T| (x ∈ L_3)}  List⌝⋅ THEN Auto))) }

1
1. T : Type
2. L_2 : T List
3. P : {x:T| (x ∈ [])}  ⟶ 𝔹
4. L_2 ≤ filter(P;[])
5. [] ≤ []
⊢ L_2 = filter(P;[]) ∈ (T List)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L$_{2}$  :  T  List
3.  P  :  \{x:T|  (x  \mmember{}  [])\}    {}\mrightarrow{}  \mBbbB{}
4.  L$_{2}$  \mleq{}  filter(P;[])
\mvdash{}  \mexists{}L$_{3}$:T  List.  (L$_{3}$  \mleq{}  []  \mwedge{}  (L$_{2}\mbackslash{}f\000Cf24  =  filter(P;L$_{3}$)))


By

---

Latex:
(InstConcl  [\mkleeneopen{}[]\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  Try  ((SubsumeC    \mkleeneopen{}\{x:T|  (x  \mmember{}  L$_{3}$)\}    List\mkleeneclose{}\mcdot{}  \000CTHEN  Auto)))

---

Home Index