---

Step * 2 of Lemma l_sum-mapfilter


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)
    ∈ ℤ)
BY
{ TACTIC:RepeatFor 2 (ParallelLast) }

1
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||) ∈ ℤ)
5. P : T ⟶ 𝔹
6. ∀[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||) ∈ ℤ)
7. f : {x:T| (x ∈ [u / v]) ∧ (↑(P x))}  ⟶ ℤ
8. l_sum(map(f;filter(P;v))) = Σ(if P v[i] then f v[i] else 0 fi  | i < ||v||) ∈ ℤ
⊢ 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:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{x:T|  (x  \mmember{}  v)  \mwedge{}  (\muparrow{}(P  x))\}    {}\mrightarrow{}  \mBbbZ{}].
          (l\_sum(map(f;filter(P;v)))  =  \mSigma{}(if  P  v[i]  then  f  v[i]  else  0  fi    |  i  <  ||v||))
\mvdash{}  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{x:T|  (x  \mmember{}  [u  /  v])  \mwedge{}  (\muparrow{}(P  x))\}    {}\mrightarrow{}  \mBbbZ{}].
        (l\_sum(map(f;if  P  u  then  [u  /  filter(P;v)]  else  filter(P;v)  fi  ))
        =  \mSigma{}(if  P  [u  /  v][i]  then  f  [u  /  v][i]  else  0  fi    |  i  <  ||v||  +  1))


By

---

Latex:
TACTIC:RepeatFor  2  (ParallelLast)

---

Home Index