---

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


1. [A] : Type
2. P : A ⟶ 𝔹
3. L : A List
4. 0 < ||filter(P;L)||
⊢ (∃x∈L. ↑(P x))
BY
{ Assert ⌜∃x:A. (x ∈ filter(P;L))⌝⋅ }

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}x:A.  (x  \mmember{}  filter(P;L))\mkleeneclose{}\mcdot{}

---

Home Index