---

Step * of Lemma rminimum-select

No Annotations
∀n,m:ℤ.  ∀x:{n..m + 1-} ⟶ ℝ. ∀e:ℝ.  ((r0 < e) ⇒ (∃i:{n..m + 1-}. (x[i] < (rminimum(n;m;i.x[i]) + e)))) supposing n ≤ m
BY
{ RepeatFor 3 ((D 0 THENA Auto)) }

1
1. n : ℤ
2. m : ℤ
3. n ≤ m
⊢ ∀x:{n..m + 1-} ⟶ ℝ. ∀e:ℝ.  ((r0 < e) ⇒ (∃i:{n..m + 1-}. (x[i] < (rminimum(n;m;i.x[i]) + e))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}n,m:\mBbbZ{}.
    \mforall{}x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}e:\mBbbR{}.    ((r0  <  e)  {}\mRightarrow{}  (\mexists{}i:\{n..m  +  1\msupminus{}\}.  (x[i]  <  (rminimum(n;m;i.x[i])  +  e)))) 
    supposing  n  \mleq{}  m


By

---

Latex:
RepeatFor  3  ((D  0  THENA  Auto))

---

Home Index