---

Step * of Lemma summand-le-l_sum

No Annotations
∀[T:Type]. ∀[L:T List]. ∀[f:{x:T| (x ∈ L)}  ⟶ ℤ].
  ∀x:{x:T| (x ∈ L)} . (f[x] ≤ l_sum(map(f;L))) supposing ∀x:{x:T| (x ∈ L)} . (0 ≤ f[x])
BY
{ (Auto
   THEN (RWO "l_sum-sum" 0 THENA Auto)
   THEN D -1
   THEN (Unhide THENA Auto)
   THEN RepeatFor 2 (D -1)
   THEN (Assert (f L[i]) ≤ Σ(f L[i] | i < ||L||) BY
               ((InstLemma `summand-le-sum` [⌜||L||⌝;⌜λ2i.f L[i]⌝]⋅ THENA Auto) THEN BHyp -1 THEN Auto))
   THEN NthHypSq (-1)
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[f:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbZ{}].
    \mforall{}x:\{x:T|  (x  \mmember{}  L)\}  .  (f[x]  \mleq{}  l\_sum(map(f;L)))  supposing  \mforall{}x:\{x:T|  (x  \mmember{}  L)\}  .  (0  \mleq{}  f[x])


By

---

Latex:
(Auto
  THEN  (RWO  "l\_sum-sum"  0  THENA  Auto)
  THEN  D  -1
  THEN  (Unhide  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  (Assert  (f  L[i])  \mleq{}  \mSigma{}(f  L[i]  |  i  <  ||L||)  BY
                          ((InstLemma  `summand-le-sum`  [\mkleeneopen{}||L||\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.f  L[i]\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  BHyp  -1
                            THEN  Auto))
  THEN  NthHypSq  (-1)
  THEN  Auto)

---

Home Index