---

Step * of Lemma length-filter-pos-iff

∀[A:Type]. ∀P:A ⟶ 𝔹. ∀L:A List.  ((∃x∈L. ↑(P x)) ⇐⇒ 0 < ||filter(P;L)||)
BY
{ Auto }

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

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

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}P:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:A  List.    ((\mexists{}x\mmember{}L.  \muparrow{}(P  x))  \mLeftarrow{}{}\mRightarrow{}  0  <  ||filter(P;L)||)


By

---

Latex:
Auto

---

Home Index