---

Step * 1 of Lemma upper-bounds-closed


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
BY
{ ((Assert lim n→∞.x = x BY Auto) THEN FLemma `rleq-limit` [-1;4] THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Set(\mBbbR{})
2.  y  :  \mBbbR{}
3.  x1  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
4.  lim  n\mrightarrow{}\minfty{}.x1[n]  =  y
5.  \mforall{}n:\mBbbN{}.  \mforall{}x@0:\mBbbR{}.    ((A  x@0)  {}\mRightarrow{}  (x@0  \mleq{}  x1[n]))
6.  x  :  \mBbbR{}
7.  A  x
\mvdash{}  x  \mleq{}  y


By

---

Latex:
((Assert  lim  n\mrightarrow{}\minfty{}.x  =  x  BY  Auto)  THEN  FLemma  `rleq-limit`  [-1;4]  THEN  Auto)

---

Home Index