---

Step * 2 of Lemma rminimum_lb


1. k : ℤ
2. n : ℤ
3. m : ℤ
4. ¬(n ≤ m)
⊢ ∀x:{n..m + 1-} ⟶ ℝ. ((n ≤ k) ⇒ (k ≤ m) ⇒ (rminimum(n;m;i.x[i]) ≤ x[k]))
BY
{ Auto }

---

Latex:

---

Latex:

1.  k  :  \mBbbZ{}
2.  n  :  \mBbbZ{}
3.  m  :  \mBbbZ{}
4.  \mneg{}(n  \mleq{}  m)
\mvdash{}  \mforall{}x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}.  ((n  \mleq{}  k)  {}\mRightarrow{}  (k  \mleq{}  m)  {}\mRightarrow{}  (rminimum(n;m;i.x[i])  \mleq{}  x[k]))


By

---

Latex:
Auto

---

Home Index