---

Step * of Lemma l_sum-mapfilter

∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹]. ∀[f:{x:T| (x ∈ L) ∧ (↑(P x))}  ⟶ ℤ].
  (l_sum(mapfilter(f;P;L)) = Σ(if P L[i] then f L[i] else 0 fi  | i < ||L||) ∈ ℤ)
BY
{ TACTIC:(Unfold `mapfilter` 0 THEN InductionOnList THEN Reduce 0) }

1
1. T : Type
⊢ ∀[P:T ⟶ 𝔹]. ∀[f:{x:T| (x ∈ []) ∧ (↑(P x))}  ⟶ ℤ].  (l_sum([]) = 0 ∈ ℤ)

2
1. T : Type
2. u : T
3. v : T List
4. ∀[P:T ⟶ 𝔹]. ∀[f:{x:T| (x ∈ v) ∧ (↑(P x))}  ⟶ ℤ].
     (l_sum(map(f;filter(P;v))) = Σ(if P v[i] then f v[i] else 0 fi  | i < ||v||) ∈ ℤ)
⊢ ∀[P:T ⟶ 𝔹]. ∀[f:{x:T| (x ∈ [u / v]) ∧ (↑(P x))}  ⟶ ℤ].
    (l_sum(map(f;if P u then [u / filter(P;v)] else filter(P;v) fi ))
    = Σ(if P [u / v][i] then f [u / v][i] else 0 fi  | i < ||v|| + 1)
    ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{x:T|  (x  \mmember{}  L)  \mwedge{}  (\muparrow{}(P  x))\}    {}\mrightarrow{}  \mBbbZ{}].
    (l\_sum(mapfilter(f;P;L))  =  \mSigma{}(if  P  L[i]  then  f  L[i]  else  0  fi    |  i  <  ||L||))


By

---

Latex:
TACTIC:(Unfold  `mapfilter`  0  THEN  InductionOnList  THEN  Reduce  0)

---

Home Index