---

Step * of Lemma i-finite-approx

∀n,m:ℕ+. ∀I:Interval.  (i-finite(i-approx(I;n)) ⇐⇒ i-finite(i-approx(I;m)))
BY
{ ((UnivCD THENA Auto)
   THEN D -1
   THEN D -2
   THEN D -1
   THEN RepUR ``i-approx i-finite`` 0
   THEN ((DVar `x' THEN Reduce 0) ORELSE Auto)
   THEN ((DVar `x1' THEN Reduce 0 THEN Auto) ORELSE Auto)) }

---

Latex:

---

Latex:
\mforall{}n,m:\mBbbN{}\msupplus{}.  \mforall{}I:Interval.    (i-finite(i-approx(I;n))  \mLeftarrow{}{}\mRightarrow{}  i-finite(i-approx(I;m)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  -1
  THEN  D  -2
  THEN  D  -1
  THEN  RepUR  ``i-approx  i-finite``  0
  THEN  ((DVar  `x'  THEN  Reduce  0)  ORELSE  Auto)
  THEN  ((DVar  `x1'  THEN  Reduce  0  THEN  Auto)  ORELSE  Auto))

---

Home Index