---

Step * of Lemma totally-bounded-bounded-above

∀[A:Set(ℝ)]. (totally-bounded(A) ⇒ bounded-above(A))
BY
{ (Unfolds ``totally-bounded bounded-above`` 0 THEN Auto THEN ((InstHyp [⌜r1⌝] (-1))⋅ 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. n : ℕ+
4. a : ℕn ⟶ ℝ
5. ∀i:ℕn. (a i ∈ A)
6. ∀x:ℝ. ((x ∈ A) ⇒ (∃i:ℕn. (|x - a i| < r1)))
⊢ ∃b:ℝ. A ≤ b

---

Latex:

---

Latex:
\mforall{}[A:Set(\mBbbR{})].  (totally-bounded(A)  {}\mRightarrow{}  bounded-above(A))


By

---

Latex:
(Unfolds  ``totally-bounded  bounded-above``  0
  THEN  Auto
  THEN  ((InstHyp  [\mkleeneopen{}r1\mkleeneclose{}]  (-1))\mcdot{}  THENA  Auto)
  THEN  ExRepD)

---

Home Index