---

Step * of Lemma bag-summation_functionality_wrt_le

∀[T:Type]. ∀[b:bag(T)]. ∀[f,g:{x:T| x ↓∈ b}  ⟶ ℤ].
  Σ(x∈b). f[x] ≤ Σ(x∈b). g[x] supposing ∀x:T. (x ↓∈ b ⇒ (f[x] ≤ g[x]))
BY
{ (RepeatFor 2 (Intro)
   THEN (InstLemma `bag-summation_functionality_wrt_le_1` [⌜{x:T| x ↓∈ b} ⌝ ;⌜b⌝]⋅
         THENA (Auto THEN BLemma `bag-subtype` THEN Auto)
         )
   THEN RepeatFor 2 (ParallelLast')
   THEN Intro
   THEN D -2
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[b:bag(T)].  \mforall{}[f,g:\{x:T|  x  \mdownarrow{}\mmember{}  b\}    {}\mrightarrow{}  \mBbbZ{}].
    \mSigma{}(x\mmember{}b).  f[x]  \mleq{}  \mSigma{}(x\mmember{}b).  g[x]  supposing  \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (f[x]  \mleq{}  g[x]))


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  (InstLemma  `bag-summation\_functionality\_wrt\_le\_1`  [\mkleeneopen{}\{x:T|  x  \mdownarrow{}\mmember{}  b\}  \mkleeneclose{}  ;\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  BLemma  `bag-subtype`  THEN  Auto)
              )
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Intro
  THEN  D  -2
  THEN  Auto)

---

Home Index