---

Step * of Lemma i-approx-rep

∀I:Interval. ∀n:ℕ+. ∀r:ℝ.  ((r ∈ i-approx(I;n)) ⇒ (∃a,b:ℝ. ((a ≤ b) ∧ (i-approx(I;n) = [a, b] ∈ Interval))))
BY
{ (InstLemma `i-approx-compact` [] THEN RepeatFor 4 (ParallelLast') THEN Auto) }

1
1. I : Interval
2. n : ℕ+
3. r : ℝ
4. r ∈ i-approx(I;n)
5. icompact(i-approx(I;n))
⊢ ∃a,b:ℝ. ((a ≤ b) ∧ (i-approx(I;n) = [a, b] ∈ Interval))

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}r:\mBbbR{}.    ((r  \mmember{}  i-approx(I;n))  {}\mRightarrow{}  (\mexists{}a,b:\mBbbR{}.  ((a  \mleq{}  b)  \mwedge{}  (i-approx(I;n)  =  [a,  b]))))


By

---

Latex:
(InstLemma  `i-approx-compact`  []  THEN  RepeatFor  4  (ParallelLast')  THEN  Auto)

---

Home Index