---

Step * 1 1 1 of Lemma hd-filter


1. T : Type
2. P : T ⟶ 𝔹
3. as : T List
4. ∃a:T. ((a ∈ as) ∧ (↑P[a]))
5. filter(λa.P[a];as) ∈ {x:T| ↑((λa.P[a]) x)}  List
6. v : {x:T| ↑((λa.P[a]) x)}  List
7. filter(λa.P[a];as) = v ∈ ({x:T| ↑((λa.P[a]) x)}  List)
8. 0 < ||v||
9. hd(v) ∈ T
⊢ ¬↑null(v)
BY
{ xxx(DVar `v' THEN Auto)xxx }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  as  :  T  List
4.  \mexists{}a:T.  ((a  \mmember{}  as)  \mwedge{}  (\muparrow{}P[a]))
5.  filter(\mlambda{}a.P[a];as)  \mmember{}  \{x:T|  \muparrow{}((\mlambda{}a.P[a])  x)\}    List
6.  v  :  \{x:T|  \muparrow{}((\mlambda{}a.P[a])  x)\}    List
7.  filter(\mlambda{}a.P[a];as)  =  v
8.  0  <  ||v||
9.  hd(v)  \mmember{}  T
\mvdash{}  \mneg{}\muparrow{}null(v)


By

---

Latex:
xxx(DVar  `v'  THEN  Auto)xxx

---

Home Index