---

Step * of Lemma rminimum-cases

No Annotations
∀n,m:ℤ.
  ∀x:{n..m + 1-} ⟶ ℝ. (¬¬(∃a:{n..m + 1-}. ((rminimum(n;m;i.x[i]) = x[a]) ∧ (∀j:{n..m + 1-}. (x[a] ≤ x[j]))))) 
  supposing n ≤ m
BY
{ RepeatFor 3 ((D 0 THENA Auto)) }

1
1. n : ℤ
2. m : ℤ
3. n ≤ m
⊢ ∀x:{n..m + 1-} ⟶ ℝ. (¬¬(∃a:{n..m + 1-}. ((rminimum(n;m;i.x[i]) = x[a]) ∧ (∀j:{n..m + 1-}. (x[a] ≤ x[j])))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}n,m:\mBbbZ{}.
    \mforall{}x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
        (\mneg{}\mneg{}(\mexists{}a:\{n..m  +  1\msupminus{}\}.  ((rminimum(n;m;i.x[i])  =  x[a])  \mwedge{}  (\mforall{}j:\{n..m  +  1\msupminus{}\}.  (x[a]  \mleq{}  x[j]))))) 
    supposing  n  \mleq{}  m


By

---

Latex:
RepeatFor  3  ((D  0  THENA  Auto))

---

Home Index