---

Step * of Lemma bag-sum-nonneg

∀[A:Type]. ∀[f:A ⟶ ℤ]. ∀[ba:bag(A)].  0 ≤ bag-sum(ba;x.f[x]) supposing ∀x:A. (0 ≤ f[x])
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[ba:bag(A)].    0  \mleq{}  bag-sum(ba;x.f[x])  supposing  \mforall{}x:A.  (0  \mleq{}  f[x])


By

---

Latex:
Auto

---

Home Index