---

Step * 3 1 of Lemma radd-list-rabs


1. L : ℝ
2. L1 : ℝ List
3. L2 : ℝ List
4. map(λx.|x|;L1) = L2 ∈ (ℝ List)
5. |radd-list(L1)| ≤ radd-list(L2)
⊢ |radd-list([L / L1])| ≤ radd-list([|L| / L2])
BY
{ (RWW "radd-list-cons r-triangle-inequality -1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  L  :  \mBbbR{}
2.  L1  :  \mBbbR{}  List
3.  L2  :  \mBbbR{}  List
4.  map(\mlambda{}x.|x|;L1)  =  L2
5.  |radd-list(L1)|  \mleq{}  radd-list(L2)
\mvdash{}  |radd-list([L  /  L1])|  \mleq{}  radd-list([|L|  /  L2])


By

---

Latex:
(RWW  "radd-list-cons  r-triangle-inequality  -1"  0  THEN  Auto)

---

Home Index