---

Step * of Lemma i-approx-finite

∀I:Interval. ∀n:ℕ+.  i-finite(i-approx(I;n))
BY
{ (Auto
   THEN (RepeatFor 2 (D 1) THEN Try (DVar `x') THEN DVar `I2' THEN Try (DVar `x'))
   THEN RepUR ``i-approx i-finite rccint`` 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (RepeatFor  2  (D  1)  THEN  Try  (DVar  `x')  THEN  DVar  `I2'  THEN  Try  (DVar  `x'))
  THEN  RepUR  ``i-approx  i-finite  rccint``  0
  THEN  Auto)

---

Home Index