---

Step * of Lemma rleq-limit

No Annotations
∀[x,y:ℕ ⟶ ℝ]. ∀[a,b:ℝ].  (a ≤ b) supposing ((∀n:ℕ. (x[n] ≤ y[n])) and lim n→∞.y[n] = b and lim n→∞.x[n] = a)
BY
{ (TACTIC:Auto THEN ((FLemma `rsub-limit` [-2; -3]) THENA Auto)) }

1
1. x : ℕ ⟶ ℝ
2. y : ℕ ⟶ ℝ
3. a : ℝ
4. b : ℝ
5. lim n→∞.x[n] = a
6. lim n→∞.y[n] = b
7. ∀n:ℕ. (x[n] ≤ y[n])
8. lim n→∞.y[n] - x[n] = b - a
⊢ a ≤ b

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x,y:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[a,b:\mBbbR{}].
    (a  \mleq{}  b)  supposing  ((\mforall{}n:\mBbbN{}.  (x[n]  \mleq{}  y[n]))  and  lim  n\mrightarrow{}\minfty{}.y[n]  =  b  and  lim  n\mrightarrow{}\minfty{}.x[n]  =  a)


By

---

Latex:
(TACTIC:Auto  THEN  ((FLemma  `rsub-limit`  [-2;  -3])  THENA  Auto))

---

Home Index