---

Step * 1 1 of Lemma rminimum-select


1. n : ℤ
⊢ ∀x:{n..(n + 0) + 1-} ⟶ ℝ. ∀e:ℝ.  ((r0 < e) ⇒ (∃i:{n..(n + 0) + 1-}. (x[i] < (x[n] + e))))
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[i]  <  (x[n]  +  e))))


By

---

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

---

Home Index