---

Step * of Lemma int-bag-product-positive

No Annotations
∀[b:bag(ℤ)]. 0 < Π(b) supposing ∀[x:ℤ]. (x ↓∈ b ⇒ 0 < x)
BY
{ Auto }

1
1. b : bag(ℤ)
2. ∀[x:ℤ]. (x ↓∈ b ⇒ 0 < x)
⊢ 0 < Π(b)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[b:bag(\mBbbZ{})].  0  <  \mPi{}(b)  supposing  \mforall{}[x:\mBbbZ{}].  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  0  <  x)


By

---

Latex:
Auto

---

Home Index