---

Step * 1 of Lemma rabs-rsum


1. n : ℤ
2. m : ℤ
3. x : {n..m + 1-} ⟶ ℝ
⊢ |radd-list(map(λi.x[i];[n, m + 1)))| ≤ radd-list(map(λi.|x[i]|;[n, m + 1)))
BY
{ (RWO "radd-list-rabs" 0
   THEN Try (Complete (Auto))
   THEN (RWW "map-map" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN GenConcl ⌜map(λx@0.|x[x@0]|;[n, m + 1)) = L ∈ (ℝ List)⌝⋅
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  x  :  \{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
\mvdash{}  |radd-list(map(\mlambda{}i.x[i];[n,  m  +  1)))|  \mleq{}  radd-list(map(\mlambda{}i.|x[i]|;[n,  m  +  1)))


By

---

Latex:
(RWO  "radd-list-rabs"  0
  THEN  Try  (Complete  (Auto))
  THEN  (RWW  "map-map"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  GenConcl  \mkleeneopen{}map(\mlambda{}x@0.|x[x@0]|;[n,  m  +  1))  =  L\mkleeneclose{}\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index