---

Step * 2 1 of Lemma length-filter-pos-iff

.....assertion..... 
1. [A] : Type
2. P : A ⟶ 𝔹
3. L : A List
4. 0 < ||filter(P;L)||
⊢ ∃x:A. (x ∈ filter(P;L))
BY
{ ((MoveToConcl (-1) THEN GenConclTerm ⌜filter(P;L)⌝⋅) THENA Auto) }

1
1. [A] : Type
2. P : A ⟶ 𝔹
3. L : A List
4. v : A List
5. filter(P;L) = v ∈ (A List)
⊢ 0 < ||v|| ⇒ (∃x:A. (x ∈ v))

---

Latex:

---

Latex:
.....assertion..... 
1.  [A]  :  Type
2.  P  :  A  {}\mrightarrow{}  \mBbbB{}
3.  L  :  A  List
4.  0  <  ||filter(P;L)||
\mvdash{}  \mexists{}x:A.  (x  \mmember{}  filter(P;L))


By

---

Latex:
((MoveToConcl  (-1)  THEN  GenConclTerm  \mkleeneopen{}filter(P;L)\mkleeneclose{}\mcdot{})  THENA  Auto)

---

Home Index