---

Step * of Lemma rmaximum_ub

∀[k,n,m:ℤ]. ∀[x:{n..m + 1-} ⟶ ℝ].  (x[k] ≤ rmaximum(n;m;i.x[i])) supposing ((k ≤ m) and (n ≤ k))
BY
{ xxx(xxxAutoxxx THEN RepeatFor 3 (MoveToConcl (-1)) THEN (Decide n ≤ m THENA Auto))xxx }

1
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])))

2
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])))

---

Latex:

---

Latex:
\mforall{}[k,n,m:\mBbbZ{}].  \mforall{}[x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}].    (x[k]  \mleq{}  rmaximum(n;m;i.x[i]))  supposing  ((k  \mleq{}  m)  and  (n  \mleq{}  k))


By

---

Latex:
xxx(xxxAutoxxx  THEN  RepeatFor  3  (MoveToConcl  (-1))  THEN  (Decide  n  \mleq{}  m  THENA  Auto))xxx

---

Home Index