---

Step * 2 of Lemma iseg_filter2


1. [T] : Type
2. aaaa : T
3. LLLL : T List
4. ∀L_2:T List. ∀P:{x:T| (x ∈ LLLL)}  ⟶ 𝔹.
     (L_2 ≤ filter(P;LLLL) ⇒ (∃L_3:T List. (L_3 ≤ LLLL ∧ (L_2 = filter(P;L_3) ∈ (T List)))))
5. L_2 : T List
6. P : {x:T| (x ∈ [aaaa / LLLL])}  ⟶ 𝔹
7. L_2 ≤ filter(P;[aaaa / LLLL])
⊢ ∃L_3:T List. (L_3 ≤ [aaaa / LLLL] ∧ (L_2 = filter(P;L_3) ∈ (T List)))
BY
{ (Decide ⌜↑null(L_2)⌝⋅ THENA Auto) }

1
1. [T] : Type
2. aaaa : T
3. LLLL : T List
4. ∀L_2:T List. ∀P:{x:T| (x ∈ LLLL)}  ⟶ 𝔹.
     (L_2 ≤ filter(P;LLLL) ⇒ (∃L_3:T List. (L_3 ≤ LLLL ∧ (L_2 = filter(P;L_3) ∈ (T List)))))
5. L_2 : T List
6. P : {x:T| (x ∈ [aaaa / LLLL])}  ⟶ 𝔹
7. L_2 ≤ filter(P;[aaaa / LLLL])
8. ↑null(L_2)
⊢ ∃L_3:T List. (L_3 ≤ [aaaa / LLLL] ∧ (L_2 = filter(P;L_3) ∈ (T List)))

2
1. [T] : Type
2. aaaa : T
3. LLLL : T List
4. ∀L_2:T List. ∀P:{x:T| (x ∈ LLLL)}  ⟶ 𝔹.
     (L_2 ≤ filter(P;LLLL) ⇒ (∃L_3:T List. (L_3 ≤ LLLL ∧ (L_2 = filter(P;L_3) ∈ (T List)))))
5. L_2 : T List
6. P : {x:T| (x ∈ [aaaa / LLLL])}  ⟶ 𝔹
7. L_2 ≤ filter(P;[aaaa / LLLL])
8. ¬↑null(L_2)
⊢ ∃L_3:T List. (L_3 ≤ [aaaa / LLLL] ∧ (L_2 = filter(P;L_3) ∈ (T List)))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  aaaa  :  T
3.  LLLL  :  T  List
4.  \mforall{}L$_{2}$:T  List.  \mforall{}P:\{x:T|  (x  \mmember{}  LLLL)\}    {}\mrightarrow{}  \mBbbB{}.
          (L$_{2}$  \mleq{}  filter(P;LLLL)  {}\mRightarrow{}  (\mexists{}L$_{3}$:T  List.  (L$\mbackslash{}\000Cff5f{3}$  \mleq{}  LLLL  \mwedge{}  (L$_{2}$  =  filter(P;L$_{3}$)))\000C))
5.  L$_{2}$  :  T  List
6.  P  :  \{x:T|  (x  \mmember{}  [aaaa  /  LLLL])\}    {}\mrightarrow{}  \mBbbB{}
7.  L$_{2}$  \mleq{}  filter(P;[aaaa  /  LLLL])
\mvdash{}  \mexists{}L$_{3}$:T  List.  (L$_{3}$  \mleq{}  [aaaa  /  LLLL]  \mwedge{}  (L$_\mbackslash{}f\000Cf7b2}$  =  filter(P;L$_{3}$)))


By

---

Latex:
(Decide  \mkleeneopen{}\muparrow{}null(L$_{2}$)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index