---

Step * of Lemma i-approx-elim

No Annotations
∀I:Interval. ∀n:ℕ+.  (i-nonvoid(i-approx(I;n)) ⇒ (∃a:ℝ. ∃b:{b:ℝ| a ≤ b} . (i-approx(I;n) = [a, b] ∈ Interval)))
BY
{ (Auto
   THEN (InstLemma `i-finite-closed-is-rccint` [⌜i-approx(I;n)⌝]⋅ THENA Auto)
   THEN HypSubst' (-1) 0
   THEN InstConcl [⌜left-endpoint(i-approx(I;n))⌝;⌜right-endpoint(i-approx(I;n))⌝]⋅
   THEN Auto
   THEN MemTypeCD
   THEN Auto) }

1
.....set predicate..... 
1. I : Interval
2. n : ℕ+
3. i-nonvoid(i-approx(I;n))
4. i-approx(I;n) ~ [left-endpoint(i-approx(I;n)), right-endpoint(i-approx(I;n))]
⊢ left-endpoint(i-approx(I;n)) ≤ right-endpoint(i-approx(I;n))

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:Interval.  \mforall{}n:\mBbbN{}\msupplus{}.    (i-nonvoid(i-approx(I;n))  {}\mRightarrow{}  (\mexists{}a:\mBbbR{}.  \mexists{}b:\{b:\mBbbR{}|  a  \mleq{}  b\}  .  (i-approx(I;n)  =  [a,  b]))\000C)


By

---

Latex:
(Auto
  THEN  (InstLemma  `i-finite-closed-is-rccint`  [\mkleeneopen{}i-approx(I;n)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  InstConcl  [\mkleeneopen{}left-endpoint(i-approx(I;n))\mkleeneclose{};\mkleeneopen{}right-endpoint(i-approx(I;n))\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index