---

Step * 3 of Lemma max-metric-mdist-from-zero


1. c : {c:ℝ| r0 ≤ c} 
2. n : ℤ
3. 0 < n
4. x : ℝ^n
5. ∀i:ℕn - 1. ((-(c) ≤ (x i)) ∧ ((x i) ≤ c)) supposing primrec(n - 1;r0;λi,r. rmax(r;|(x i) - r0|)) ≤ c
6. primrec(n - 1;r0;λi,r. rmax(r;|(x i) - r0|)) ≤ c supposing ∀i:ℕn - 1. ((-(c) ≤ (x i)) ∧ ((x i) ≤ c))
7. ∀i:ℕn. ((-(c) ≤ (x i)) ∧ ((x i) ≤ c))
⊢ (r0 - c) ≤ (x (n - 1))
BY
{ (D -1 With ⌜n - 1⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  c  :  \{c:\mBbbR{}|  r0  \mleq{}  c\} 
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  x  :  \mBbbR{}\^{}n
5.  \mforall{}i:\mBbbN{}n  -  1.  ((-(c)  \mleq{}  (x  i))  \mwedge{}  ((x  i)  \mleq{}  c))  supposing  primrec(n  -  1;r0;\mlambda{}i,r.  rmax(r;|(x  i)  -  r0|))  \000C\mleq{}  c
6.  primrec(n  -  1;r0;\mlambda{}i,r.  rmax(r;|(x  i)  -  r0|))  \mleq{}  c  supposing  \mforall{}i:\mBbbN{}n  -  1.  ((-(c)  \mleq{}  (x  i))  \mwedge{}  ((x  i)  \mleq{}  \000Cc))
7.  \mforall{}i:\mBbbN{}n.  ((-(c)  \mleq{}  (x  i))  \mwedge{}  ((x  i)  \mleq{}  c))
\mvdash{}  (r0  -  c)  \mleq{}  (x  (n  -  1))


By

---

Latex:
(D  -1  With  \mkleeneopen{}n  -  1\mkleeneclose{}    THEN  Auto)

---

Home Index