---

Step * 1 of Lemma l_sum-mapfilter-upto


1. n : ℕ
2. P : ℕn ⟶ 𝔹
3. f : {x:ℕn| ↑(P x)}  ⟶ ℤ
⊢ l_sum(mapfilter(f;P;upto(n))) = Σ(if P i then f i else 0 fi  | i < n) ∈ ℤ
BY
{ ((InstLemma `l_sum-mapfilter` [⌜ℕn⌝;⌜upto(n)⌝;⌜P⌝;⌜f⌝]⋅ THENA Auto)
   THEN NthHypEq (-1)
   THEN RepeatFor 2 ((EqCD THEN Auto))) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  P  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbB{}
3.  f  :  \{x:\mBbbN{}n|  \muparrow{}(P  x)\}    {}\mrightarrow{}  \mBbbZ{}
\mvdash{}  l\_sum(mapfilter(f;P;upto(n)))  =  \mSigma{}(if  P  i  then  f  i  else  0  fi    |  i  <  n)


By

---

Latex:
((InstLemma  `l\_sum-mapfilter`  [\mkleeneopen{}\mBbbN{}n\mkleeneclose{};\mkleeneopen{}upto(n)\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  NthHypEq  (-1)
  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index