---

Step * 1 1 of Lemma totally-bounded-sup


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
BY
{ Assert ⌜x < (x + (r(2) * e))⌝⋅ }

1
.....assertion..... 
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)))
⊢ x < (x + (r(2) * e))

2
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)))
13. x < (x + (r(2) * e))
⊢ (∃a:ℝ. ((a ∈ A) ∧ (x < a))) ∨ A ≤ y

---

Latex:

---

Latex:

1.  [A]  :  Set(\mBbbR{})
2.  \mforall{}e:\mBbbR{}
          ((r0  <  e)
          {}\mRightarrow{}  (\mexists{}n:\mBbbN{}\msupplus{}.  \mexists{}a:\mBbbN{}n  {}\mrightarrow{}  \mBbbR{}.  ((\mforall{}i:\mBbbN{}n.  (a  i  \mmember{}  A))  \mwedge{}  (\mforall{}x:\mBbbR{}.  ((x  \mmember{}  A)  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}n.  (|x  -  a  i|  <  e)))))))
3.  x  :  \mBbbR{}
4.  y  :  \mBbbR{}
5.  x  <  y
6.  e  :  \mBbbR{}
7.  r0  <  e
8.  (x  +  (r(4)  *  e))  =  y
9.  n  :  \mBbbN{}\msupplus{}
10.  a  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbR{}
11.  \mforall{}i:\mBbbN{}n.  (a  i  \mmember{}  A)
12.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  A)  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}n.  (|x  -  a  i|  <  e)))
\mvdash{}  (\mexists{}a:\mBbbR{}.  ((a  \mmember{}  A)  \mwedge{}  (x  <  a)))  \mvee{}  A  \mleq{}  y


By

---

Latex:
Assert  \mkleeneopen{}x  <  (x  +  (r(2)  *  e))\mkleeneclose{}\mcdot{}

---

Home Index