---

Step * of Lemma l_sum-mapfilter-upto

No Annotations
∀[n:ℕ]. ∀[P:ℕn ⟶ 𝔹]. ∀[f:{x:ℕn| ↑(P x)}  ⟶ ℤ].
  (l_sum(mapfilter(f;P;upto(n))) = Σ(if P i then f i else 0 fi  | i < n) ∈ ℤ)
BY
{ Auto }

1
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) ∈ ℤ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  \mforall{}[P:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{x:\mBbbN{}n|  \muparrow{}(P  x)\}    {}\mrightarrow{}  \mBbbZ{}].
    (l\_sum(mapfilter(f;P;upto(n)))  =  \mSigma{}(if  P  i  then  f  i  else  0  fi    |  i  <  n))


By

---

Latex:
Auto

---

Home Index