---

Step * 1 1 1 1 2 1 1 1 of Lemma fset-find_wf


1. T : Type
2. eq : EqDecider(T)
3. P : T ⟶ 𝔹
4. s : Base
5. s ∈ T List
6. ∃x:T. ((x ∈ s) ∧ (↑(P x)))
7. filter(P;s) ∈ {x:{x:T| (x ∈ s)} | ↑(P x)}  List
⊢ ||filter(P;s)|| ≥ 1 
BY
{ ((Assert ⌜0 < ||filter(P;s)||⌝⋅ THENM Auto)
   THEN BLemma `length-filter-pos`
   THEN Auto
   THEN BLemma `l_exists_iff`
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  P  :  T  {}\mrightarrow{}  \mBbbB{}
4.  s  :  Base
5.  s  \mmember{}  T  List
6.  \mexists{}x:T.  ((x  \mmember{}  s)  \mwedge{}  (\muparrow{}(P  x)))
7.  filter(P;s)  \mmember{}  \{x:\{x:T|  (x  \mmember{}  s)\}  |  \muparrow{}(P  x)\}    List
\mvdash{}  ||filter(P;s)||  \mgeq{}  1 


By

---

Latex:
((Assert  \mkleeneopen{}0  <  ||filter(P;s)||\mkleeneclose{}\mcdot{}  THENM  Auto)
  THEN  BLemma  `length-filter-pos`
  THEN  Auto
  THEN  BLemma  `l\_exists\_iff`
  THEN  Auto)

---

Home Index