---

Step * of Lemma rminimum_lb

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

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

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

---

Latex:

---

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


By

---

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

---

Home Index