Step
*
of Lemma
implies-approx-compact
No Annotations
∀I:Interval. ∀n:ℕ+. ((∃r:ℝ. (r ∈ i-approx(I;n)))
⇒ icompact(i-approx(I;n)))
BY
{ (Auto THEN D -1 THEN FLemma `i-approx-compact` [-1] THEN Auto) }
Latex:
Latex:
No Annotations
\mforall{}I:Interval. \mforall{}n:\mBbbN{}\msupplus{}. ((\mexists{}r:\mBbbR{}. (r \mmember{} i-approx(I;n))) {}\mRightarrow{} icompact(i-approx(I;n)))
By
Latex:
(Auto THEN D -1 THEN FLemma `i-approx-compact` [-1] THEN Auto)
Home
Index