Step
*
of Lemma
i-approx-of-compact
∀I:Interval. (icompact(I)
⇒ (∀n:ℕ+. (i-approx(I;n) = I ∈ Interval)))
BY
{ (Auto
THEN RepUR ``icompact i-finite i-closed`` 2
THEN RepeatFor 2 (D 1)
THEN All Reduce
THEN Auto
THEN D 1
THEN All Reduce
THEN Auto
THEN D 2
THEN All Reduce
THEN Auto
THEN D 2
THEN All Reduce
THEN Auto) }
Latex:
Latex:
\mforall{}I:Interval. (icompact(I) {}\mRightarrow{} (\mforall{}n:\mBbbN{}\msupplus{}. (i-approx(I;n) = I)))
By
Latex:
(Auto
THEN RepUR ``icompact i-finite i-closed`` 2
THEN RepeatFor 2 (D 1)
THEN All Reduce
THEN Auto
THEN D 1
THEN All Reduce
THEN Auto
THEN D 2
THEN All Reduce
THEN Auto
THEN D 2
THEN All Reduce
THEN Auto)
Home
Index