---

Step * of Lemma radd-list-rabs

∀L:ℝ List. (|radd-list(L)| ≤ radd-list(map(λx.|x|;L)))
BY
{ (InductionOnListA THEN Reduce 0) }

1
.....wf..... 
λL.(|radd-list(L)| ≤ radd-list(map(λx.|x|;L))) ∈ (ℝ List) ⟶ ℙ

2
|r0| ≤ r0

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

4
.....wf..... 
1. L : ℝ
2. L1 : ℝ List
⊢ istype(|radd-list(L1)| ≤ radd-list(map(λx.|x|;L1)))

---

Latex:

---

Latex:
\mforall{}L:\mBbbR{}  List.  (|radd-list(L)|  \mleq{}  radd-list(map(\mlambda{}x.|x|;L)))


By

---

Latex:
(InductionOnListA  THEN  Reduce  0)

---

Home Index