---

Step * of Lemma l_sum-triangle-inequality-general

∀[T:Type]. ∀[L:T List]. ∀[x,y:ℤ]. ∀[f,g:T ⟶ ℤ].
  (|(l_sum(map(λa.f[a];L)) + x) - l_sum(map(λa.g[a];L)) + y| ≤ (l_sum(map(λa.|f[a] - g[a]|;L)) + |x - y|))
BY
{ (InstLemma `list_accum-triangle-inequality` []
   THEN RepeatFor 6 (ParallelLast')
   THEN RWO "l_sum_as_accum" (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[x,y:\mBbbZ{}].  \mforall{}[f,g:T  {}\mrightarrow{}  \mBbbZ{}].
    (|(l\_sum(map(\mlambda{}a.f[a];L))  +  x)  -  l\_sum(map(\mlambda{}a.g[a];L))  +  y|  \mleq{}  (l\_sum(map(\mlambda{}a.|f[a]  -  g[a]|;L))
      +  |x  -  y|))


By

---

Latex:
(InstLemma  `list\_accum-triangle-inequality`  []
  THEN  RepeatFor  6  (ParallelLast')
  THEN  RWO  "l\_sum\_as\_accum"  (-1)
  THEN  Auto)

---

Home Index