---

Step * of Lemma bag-summation-equal-implies-all-equal

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

1
1. [T] : Type
2. [b] : bag(T)
3. [f] : {x:T| x ↓∈ b}  ⟶ ℤ
4. [g] : {x:T| x ↓∈ b}  ⟶ ℤ
5. (∀x:{x:T| x ↓∈ b} . (x ↓∈ b ⇒ (f[x] = g[x] ∈ ℤ))) supposing 
      ((Σ(x∈b). g[x] ≤ Σ(x∈b). f[x]) and 
      (∀x:{x:T| x ↓∈ b} . (x ↓∈ b ⇒ (f[x] ≤ g[x]))))
⊢ (∀x:T. (x ↓∈ b ⇒ (f[x] = g[x] ∈ ℤ))) supposing ((Σ(x∈b). g[x] ≤ Σ(x∈b). f[x]) and (∀x:T. (x ↓∈ b ⇒ (f[x] ≤ g[x]))))

---

Latex:

---

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


By

---

Latex:
TACTIC:(RepeatFor  2  (Intro)
                THEN  (InstLemma  `bag-summation-equal-implies-all-equal-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'))

---

Home Index