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