---

Step * 1 1 1 of Lemma totally-bounded-bounded-above


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. n : ℕ+
4. a : ℕn ⟶ ℝ
5. ∀i:ℕn. (a i ∈ A)
6. ∀x:ℝ. ((x ∈ A) ⇒ (∃i:ℕn. (|x - a i| < r1)))
7. x : ℝ
8. x ∈ A
9. i : ℕn
10. |x - a i| < r1
⊢ x ≤ (rmaximum(0;n - 1;i.a i) + r1)
BY
{ Assert ⌜x < ((a i) + r1)⌝⋅ }

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. n : ℕ+
4. a : ℕn ⟶ ℝ
5. ∀i:ℕn. (a i ∈ A)
6. ∀x:ℝ. ((x ∈ A) ⇒ (∃i:ℕn. (|x - a i| < r1)))
7. x : ℝ
8. x ∈ A
9. i : ℕn
10. |x - a i| < r1
⊢ x < ((a i) + r1)

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. n : ℕ+
4. a : ℕn ⟶ ℝ
5. ∀i:ℕn. (a i ∈ A)
6. ∀x:ℝ. ((x ∈ A) ⇒ (∃i:ℕn. (|x - a i| < r1)))
7. x : ℝ
8. x ∈ A
9. i : ℕn
10. |x - a i| < r1
11. x < ((a i) + r1)
⊢ x ≤ (rmaximum(0;n - 1;i.a i) + r1)

---

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.  n  :  \mBbbN{}\msupplus{}
4.  a  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbR{}
5.  \mforall{}i:\mBbbN{}n.  (a  i  \mmember{}  A)
6.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  A)  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}n.  (|x  -  a  i|  <  r1)))
7.  x  :  \mBbbR{}
8.  x  \mmember{}  A
9.  i  :  \mBbbN{}n
10.  |x  -  a  i|  <  r1
\mvdash{}  x  \mleq{}  (rmaximum(0;n  -  1;i.a  i)  +  r1)


By

---

Latex:
Assert  \mkleeneopen{}x  <  ((a  i)  +  r1)\mkleeneclose{}\mcdot{}

---

Home Index