---

Step * of Lemma approx-in-interval_wf

∀l:ℝ. ∀u:{u:ℝ| l ≤ u} . ∀x:{x:ℝ| x ∈ [l, u]} . ∀n:ℕ+.
  (approx-in-interval(l;u;x;n) ∈ {y:ℝ| (y ∈ [l, u]) ∧ (|x - y| ≤ (r(2)/r(n)))} )
BY
{ (Auto
   THEN RepUR ``approx-in-interval`` 0
   THEN RepeatFor 2 ((CallByValueReduce 0⋅ THENA Auto))
   THEN AutoSplit
   THEN ((AutoSplit THEN MemTypeCD THEN Auto) ORELSE (MemTypeCD THEN Auto))) }

1
1. l : ℝ
2. u : {u:ℝ| l ≤ u} 
3. x : {x:ℝ| x ∈ [l, u]} 
4. n : ℕ+
5. (x n) * 2 < (l (2 * n)) + 2
6. l ≤ l
7. l ≤ u
⊢ |x - l| ≤ (r(2)/r(n))

2
1. l : ℝ
2. u : {u:ℝ| l ≤ u} 
3. x : {x:ℝ| x ∈ [l, u]} 
4. n : ℕ+
5. ¬(x n) * 2 < (l (2 * n)) + 2
6. (u (2 * n)) - 2 < (x n) * 2
7. l ≤ u
8. u ≤ u
⊢ |x - u| ≤ (r(2)/r(n))

3
1. l : ℝ
2. u : {u:ℝ| l ≤ u} 
3. x : {x:ℝ| x ∈ [l, u]} 
4. n : ℕ+
5. ¬(u (2 * n)) - 2 < (x n) * 2
6. ¬(x n) * 2 < (l (2 * n)) + 2
⊢ l ≤ (r(x n))/2 * n

4
1. l : ℝ
2. u : {u:ℝ| l ≤ u} 
3. x : {x:ℝ| x ∈ [l, u]} 
4. n : ℕ+
5. ¬(u (2 * n)) - 2 < (x n) * 2
6. ¬(x n) * 2 < (l (2 * n)) + 2
7. l ≤ (r(x n))/2 * n
⊢ (r(x n))/2 * n ≤ u

5
1. l : ℝ
2. u : {u:ℝ| l ≤ u} 
3. x : {x:ℝ| x ∈ [l, u]} 
4. n : ℕ+
5. ¬(u (2 * n)) - 2 < (x n) * 2
6. ¬(x n) * 2 < (l (2 * n)) + 2
7. l ≤ (r(x n))/2 * n
8. (r(x n))/2 * n ≤ u
⊢ |x - (r(x n))/2 * n| ≤ (r(2)/r(n))

---

Latex:

---

Latex:
\mforall{}l:\mBbbR{}.  \mforall{}u:\{u:\mBbbR{}|  l  \mleq{}  u\}  .  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [l,  u]\}  .  \mforall{}n:\mBbbN{}\msupplus{}.
    (approx-in-interval(l;u;x;n)  \mmember{}  \{y:\mBbbR{}|  (y  \mmember{}  [l,  u])  \mwedge{}  (|x  -  y|  \mleq{}  (r(2)/r(n)))\}  )


By

---

Latex:
(Auto
  THEN  RepUR  ``approx-in-interval``  0
  THEN  RepeatFor  2  ((CallByValueReduce  0\mcdot{}  THENA  Auto))
  THEN  AutoSplit
  THEN  ((AutoSplit  THEN  MemTypeCD  THEN  Auto)  ORELSE  (MemTypeCD  THEN  Auto)))

---

Home Index