Step
*
of Lemma
i-approx-closed
∀I:Interval. ∀n:ℕ+.  i-closed(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-closed rccint`` 0
   THEN Auto) }
Latex:
Latex:
\mforall{}I:Interval.  \mforall{}n:\mBbbN{}\msupplus{}.    i-closed(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-closed  rccint``  0
  THEN  Auto)
Home
Index