---

Step * of Lemma l_sum-split

No Annotations
∀[A:Type]. ∀[L:A List]. ∀[f:{a:A| (a ∈ L)}  ⟶ ℤ]. ∀[P:{a:A| (a ∈ L)}  ⟶ 𝔹].
  (l_sum(map(f;L)) = (l_sum(map(f;filter(P;L))) + l_sum(map(f;filter(λx.(¬b(P x));L)))) ∈ ℤ)
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Auto
   THEN ((InstHyp [⌜f⌝;⌜P⌝] 4⋅ THENA Auto) THEN HypSubst' (-1) 0)
   THEN BoolCase ⌜P u⌝⋅
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  ((InstHyp  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]  4\mcdot{}  THENA  Auto)  THEN  HypSubst'  (-1)  0)
  THEN  BoolCase  \mkleeneopen{}P  u\mkleeneclose{}\mcdot{}
  THEN  Reduce  0
  THEN  Auto)

---

Home Index