---

Step * of Lemma rmax-limit

∀x,y:ℕ ⟶ ℝ. ∀a,b:ℝ.  (lim n→∞.x[n] = a ⇒ lim n→∞.y[n] = b ⇒ lim n→∞.rmax(x[n];y[n]) = rmax(a;b))
BY
{ (Auto
   THEN (All (Unfold `converges-to`))
   THEN Auto
   THEN ∀h:hyp. (((InstHyp [⌜k⌝] h)⋅ THENA Auto') THEN D -1 THEN Thin h) 
   THEN (InstConcl [⌜imax(N;N1)⌝])⋅
   THEN Auto
   THEN Try ((BLemma `imax_ub` THEN Auto))
   THEN ((FLemma `imax_lb` [-1]) THENA Auto)
   THEN ∀h:hyp. (((InstHyp [⌜n⌝] h)⋅ THENA Auto) THEN Thin h) ) }

1
1. x : ℕ ⟶ ℝ
2. y : ℕ ⟶ ℝ
3. a : ℝ
4. b : ℝ
5. k : ℕ+
6. N : ℕ
7. N1 : ℕ
8. n : ℕ
9. imax(N;N1) ≤ n
10. (N ≤ n) ∧ (N1 ≤ n)
11. |x[n] - a| ≤ (r1/r(k))
12. |y[n] - b| ≤ (r1/r(k))
⊢ |rmax(x[n];y[n]) - rmax(a;b)| ≤ (r1/r(k))

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}a,b:\mBbbR{}.    (lim  n\mrightarrow{}\minfty{}.x[n]  =  a  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.y[n]  =  b  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.rmax(x[n];y[n])  =  rmax(a;b))


By

---

Latex:
(Auto
  THEN  (All  (Unfold  `converges-to`))
  THEN  Auto
  THEN  \mforall{}h:hyp.  (((InstHyp  [\mkleeneopen{}k\mkleeneclose{}]  h)\mcdot{}  THENA  Auto')  THEN  D  -1  THEN  Thin  h) 
  THEN  (InstConcl  [\mkleeneopen{}imax(N;N1)\mkleeneclose{}])\mcdot{}
  THEN  Auto
  THEN  Try  ((BLemma  `imax\_ub`  THEN  Auto))
  THEN  ((FLemma  `imax\_lb`  [-1])  THENA  Auto)
  THEN  \mforall{}h:hyp.  (((InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  h)\mcdot{}  THENA  Auto)  THEN  Thin  h)  )

---

Home Index