---

Step * 3 of Lemma radd-list-rabs


1. L : ℝ
2. L1 : ℝ List
3. |radd-list(L1)| ≤ radd-list(map(λx.|x|;L1))
⊢ |radd-list([L / L1])| ≤ radd-list([|L| / map(λx.|x|;L1)])
BY
{ (MoveToConcl (-1) THEN GenConcl ⌜map(λx.|x|;L1) = L2 ∈ (ℝ List)⌝⋅ THEN Auto) }

1
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])

---

Latex:

---

Latex:

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


By

---

Latex:
(MoveToConcl  (-1)  THEN  GenConcl  \mkleeneopen{}map(\mlambda{}x.|x|;L1)  =  L2\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index