---

Step * 1 of Lemma totally-bounded-sup


1. [A] : Set(ℝ)
2. totally-bounded(A)
3. x : ℝ
4. y : ℝ
5. x < y
⊢ (∃a:ℝ. ((a ∈ A) ∧ (x < a))) ∨ A ≤ y
BY
{ (Unfold `totally-bounded` 2
   THEN (Assert ∃e:ℝ. ((r0 < e) ∧ ((x + (r(4) * e)) = y)) BY
               ((InstConcl [⌜(y - x/r(4))⌝])⋅ THEN Auto THEN nRMul ⌜r(4)⌝ 0⋅ THEN Auto THEN nRAdd ⌜x⌝ 0⋅ THEN Auto))
   THEN ExRepD
   THEN ((InstHyp [⌜e⌝] 2)⋅ THENA Auto)
   THEN ExRepD) }

1
1. [A] : Set(ℝ)
2. ∀e:ℝ. ((r0 < e) ⇒ (∃n:ℕ+. ∃a:ℕn ⟶ ℝ. ((∀i:ℕn. (a i ∈ A)) ∧ (∀x:ℝ. ((x ∈ A) ⇒ (∃i:ℕn. (|x - a i| < e)))))))
3. x : ℝ
4. y : ℝ
5. x < y
6. e : ℝ
7. r0 < e
8. (x + (r(4) * e)) = y
9. n : ℕ+
10. a : ℕn ⟶ ℝ
11. ∀i:ℕn. (a i ∈ A)
12. ∀x:ℝ. ((x ∈ A) ⇒ (∃i:ℕn. (|x - a i| < e)))
⊢ (∃a:ℝ. ((a ∈ A) ∧ (x < a))) ∨ A ≤ y

---

Latex:

---

Latex:

1.  [A]  :  Set(\mBbbR{})
2.  totally-bounded(A)
3.  x  :  \mBbbR{}
4.  y  :  \mBbbR{}
5.  x  <  y
\mvdash{}  (\mexists{}a:\mBbbR{}.  ((a  \mmember{}  A)  \mwedge{}  (x  <  a)))  \mvee{}  A  \mleq{}  y


By

---

Latex:
(Unfold  `totally-bounded`  2
  THEN  (Assert  \mexists{}e:\mBbbR{}.  ((r0  <  e)  \mwedge{}  ((x  +  (r(4)  *  e))  =  y))  BY
                          ((InstConcl  [\mkleeneopen{}(y  -  x/r(4))\mkleeneclose{}])\mcdot{}
                            THEN  Auto
                            THEN  nRMul  \mkleeneopen{}r(4)\mkleeneclose{}  0\mcdot{}
                            THEN  Auto
                            THEN  nRAdd  \mkleeneopen{}x\mkleeneclose{}  0\mcdot{}
                            THEN  Auto))
  THEN  ExRepD
  THEN  ((InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  2)\mcdot{}  THENA  Auto)
  THEN  ExRepD)

---

Home Index