---

Step * of Lemma lsum-split

No Annotations
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)}  ⟶ 𝔹]. ∀[f:{x:T| (x ∈ L)}  ⟶ ℤ].
  (Σ(f[x] | x ∈ L) = (Σ(f[x] | x ∈ filter(λx.P[x];L)) + Σ(f[x] | x ∈ filter(λx.(¬bP[x]);L))) ∈ ℤ)
BY
{ ((InstLemma `l_sum-split` [] THEN RepeatFor 2 (ParallelLast'))
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN (InstHyp [⌜f⌝;⌜P⌝] 3⋅ THENA Auto)
   THEN Thin 3) }

1
1. T : Type
2. L : T List
3. P : {x:T| (x ∈ L)}  ⟶ 𝔹
4. f : {x:T| (x ∈ L)}  ⟶ ℤ
5. l_sum(map(f;L)) = (l_sum(map(f;filter(P;L))) + l_sum(map(f;filter(λx.(¬b(P x));L)))) ∈ ℤ
⊢ Σ(f[x] | x ∈ L) = (Σ(f[x] | x ∈ filter(λx.P[x];L)) + Σ(f[x] | x ∈ filter(λx.(¬bP[x]);L))) ∈ ℤ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbZ{}].
    (\mSigma{}(f[x]  |  x  \mmember{}  L)  =  (\mSigma{}(f[x]  |  x  \mmember{}  filter(\mlambda{}x.P[x];L))  +  \mSigma{}(f[x]  |  x  \mmember{}  filter(\mlambda{}x.(\mneg{}\msubb{}P[x]);L))))


By

---

Latex:
((InstLemma  `l\_sum-split`  []  THEN  RepeatFor  2  (ParallelLast'))
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (InstHyp  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  Thin  3)

---

Home Index