---

Step * 2 of Lemma rmaximum_ub


1. k : ℤ
2. n : ℤ
3. m : ℤ
4. ¬(n ≤ m)
⊢ ∀x:{n..m + 1-} ⟶ ℝ. ((n ≤ k) ⇒ (k ≤ m) ⇒ (x[k] ≤ rmaximum(n;m;i.x[i])))
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{}  (x[k]  \mleq{}  rmaximum(n;m;i.x[i])))


By

---

Latex:
Auto

---

Home Index