---

Step * 1 1 of Lemma rmaximum-select


1. n : ℤ
⊢ ∀x:{n..(n + 0) + 1-} ⟶ ℝ. ∀e:ℝ.  ((r0 < e) ⇒ (∃i:{n..(n + 0) + 1-}. ((x[n] - e) < x[i])))
BY
{ (Auto⋅ THEN InstConcl [⌜n⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
\mvdash{}  \mforall{}x:\{n..(n  +  0)  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}e:\mBbbR{}.    ((r0  <  e)  {}\mRightarrow{}  (\mexists{}i:\{n..(n  +  0)  +  1\msupminus{}\}.  ((x[n]  -  e)  <  x[i])))


By

---

Latex:
(Auto\mcdot{}  THEN  InstConcl  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index