---

Step * of Lemma upper-bounds-closed

∀[A:Set(ℝ)]. closed-rset(upper-bounds(A))
BY
{ (RepUR ``member-closure closed-rset upper-bounds rset-member upper-bound`` 0 THEN Auto THEN ExRepD) }

1
1. A : Set(ℝ)
2. y : ℝ
3. x1 : ℕ ⟶ ℝ
4. lim n→∞.x1[n] = y
5. ∀n:ℕ. ∀x@0:ℝ.  ((A x@0) ⇒ (x@0 ≤ x1[n]))
6. x : ℝ
7. A x
⊢ x ≤ y

---

Latex:

---

Latex:
\mforall{}[A:Set(\mBbbR{})].  closed-rset(upper-bounds(A))


By

---

Latex:
(RepUR  ``member-closure  closed-rset  upper-bounds  rset-member  upper-bound``  0  THEN  Auto  THEN  ExRepD)

---

Home Index