---

Step * of Lemma radd-list_functionality_wrt_rleq

∀[L1,L2:ℝ List].  radd-list(L1) ≤ radd-list(L2) supposing (||L1|| = ||L2|| ∈ ℤ) ∧ (∀i:ℕ||L1||. (L1[i] ≤ L2[i]))
BY
{ (RepeatFor 2 (InductionOnList) THEN Reduce 0 THEN Auto' THEN RWO "radd-list-cons" 0 THEN Auto) }

1
1. u : ℝ
2. v : ℝ List
3. ∀[L2:ℝ List]. radd-list(v) ≤ radd-list(L2) supposing (||v|| = ||L2|| ∈ ℤ) ∧ (∀i:ℕ||v||. (v[i] ≤ L2[i]))
4. u1 : ℝ
5. v1 : ℝ List
6. radd-list([u / v]) ≤ radd-list(v1) supposing (||[u / v]|| = ||v1|| ∈ ℤ) ∧ (∀i:ℕ||[u / v]||. ([u / v][i] ≤ v1[i]))
7. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
8. ∀i:ℕ||v|| + 1. ([u / v][i] ≤ [u1 / v1][i])
⊢ (u + radd-list(v)) ≤ (u1 + radd-list(v1))

---

Latex:

---

Latex:
\mforall{}[L1,L2:\mBbbR{}  List].
    radd-list(L1)  \mleq{}  radd-list(L2)  supposing  (||L1||  =  ||L2||)  \mwedge{}  (\mforall{}i:\mBbbN{}||L1||.  (L1[i]  \mleq{}  L2[i]))


By

---

Latex:
(RepeatFor  2  (InductionOnList)  THEN  Reduce  0  THEN  Auto'  THEN  RWO  "radd-list-cons"  0  THEN  Auto)

---

Home Index