---

Step * 1 of Lemma i-approx-monotonic


1. I : Interval@i
2. n : ℕ+@i
3. m : ℕ+@i
4. n ≤ m
5. x : ℝ@i
6. x ∈ i-approx(I;n)@i
7. r(n) ≤ r(m)
8. r(-m) ≤ r(-n)
9. (r1/r(m)) ≤ (r1/r(n))
⊢ x ∈ i-approx(I;m)
BY
{ (Thin 4
   THEN (D 1⋅
         THEN (D 1 THENL [D 1; Id])
         THEN (D 2 THENL [D 2; Id])
         THEN All (RepUR ``i-approx``)
         THEN Auto
         THEN (All (RepUR ``i-member``) THEN Auto THEN Try (((RWO "-2" 0 ORELSE RWO "-1" 0) THEN Auto)))⋅)⋅
   ) }

---

Latex:

---

Latex:

1.  I  :  Interval@i
2.  n  :  \mBbbN{}\msupplus{}@i
3.  m  :  \mBbbN{}\msupplus{}@i
4.  n  \mleq{}  m
5.  x  :  \mBbbR{}@i
6.  x  \mmember{}  i-approx(I;n)@i
7.  r(n)  \mleq{}  r(m)
8.  r(-m)  \mleq{}  r(-n)
9.  (r1/r(m))  \mleq{}  (r1/r(n))
\mvdash{}  x  \mmember{}  i-approx(I;m)


By

---

Latex:
(Thin  4
  THEN  (D  1\mcdot{}
              THEN  (D  1  THENL  [D  1;  Id])
              THEN  (D  2  THENL  [D  2;  Id])
              THEN  All  (RepUR  ``i-approx``)
              THEN  Auto
              THEN  (All  (RepUR  ``i-member``)
                          THEN  Auto
                          THEN  Try  (((RWO  "-2"  0  ORELSE  RWO  "-1"  0)  THEN  Auto)))\mcdot{})\mcdot{}
  )

---

Home Index