---

Step * of Lemma non_neg_sum-map

∀[T:Type]. ∀[f:T ⟶ ℤ]. ∀[L:T List].  0 ≤ Σf[x] for x ∈ L supposing (∀x∈L.0 ≤ f[x])
BY
{ ((Auto THEN Unfold `sum-map` 0) THEN BLemma `non_neg_sum` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[L:T  List].    0  \mleq{}  \mSigma{}f[x]  for  x  \mmember{}  L  supposing  (\mforall{}x\mmember{}L.0  \mleq{}  f[x])


By

---

Latex:
((Auto  THEN  Unfold  `sum-map`  0)  THEN  BLemma  `non\_neg\_sum`  THEN  Auto)

---

Home Index