---

Step * 2 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))
6. (r0 - c) ≤ (x (n - 1))
7. (x (n - 1)) ≤ (r0 + c)
8. i : ℕn
9. primrec(n - 1;r0;λi,r. rmax(r;|(x i) - r0|)) ≤ c
10. ∀i:ℕn - 1. ((-(c) ≤ (x i)) ∧ ((x i) ≤ c))
⊢ (x i) ≤ c
BY
{ (Decide ⌜i < n - 1⌝⋅ THEN Auto THEN Subst' i ~ n - 1 0 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))
6.  (r0  -  c)  \mleq{}  (x  (n  -  1))
7.  (x  (n  -  1))  \mleq{}  (r0  +  c)
8.  i  :  \mBbbN{}n
9.  primrec(n  -  1;r0;\mlambda{}i,r.  rmax(r;|(x  i)  -  r0|))  \mleq{}  c
10.  \mforall{}i:\mBbbN{}n  -  1.  ((-(c)  \mleq{}  (x  i))  \mwedge{}  ((x  i)  \mleq{}  c))
\mvdash{}  (x  i)  \mleq{}  c


By

---

Latex:
(Decide  \mkleeneopen{}i  <  n  -  1\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  Subst'  i  \msim{}  n  -  1  0  THEN  Auto)

---

Home Index