---

Step * of Lemma lsum_wf

No Annotations
∀[T:Type]. ∀[L:T List]. ∀[f:{x:T| (x ∈ L)}  ⟶ ℤ].  (Σ(f[x] | x ∈ L) ∈ ℤ)
BY
{ (((Intros THEN Unfold `lsum` 0) THEN (Assert L ∈ {x:T| (x ∈ L)}  List BY Auto)) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[f:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbZ{}].    (\mSigma{}(f[x]  |  x  \mmember{}  L)  \mmember{}  \mBbbZ{})


By

---

Latex:
(((Intros  THEN  Unfold  `lsum`  0)  THEN  (Assert  L  \mmember{}  \{x:T|  (x  \mmember{}  L)\}    List  BY  Auto))  THEN  Auto)

---

Home Index