---

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


1. A : Type
2. P : A ⟶ 𝔹
3. L : A List
4. (∃x∈L. ↑(P x))
⊢ 0 < ||filter(P;L)||
BY
{ (BLemma `length-filter-pos` THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(BLemma  `length-filter-pos`  THEN  Auto)

---

Home Index