---

Step * of Lemma rminimum-positive

∀n,m:ℤ.  ∀x:{n..m + 1-} ⟶ ℝ. (r0 < rminimum(n;m;i.x[i]) ⇐⇒ ∀i:{n..m + 1-}. (r0 < x[i])) supposing n ≤ m
BY
{ Auto }

1
1. n : ℤ
2. m : ℤ
3. n ≤ m
4. x : {n..m + 1-} ⟶ ℝ
5. r0 < rminimum(n;m;i.x[i])
6. i : {n..m + 1-}
⊢ r0 < x[i]

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index