---

Step * 2 of Lemma max-metric-mdist-from-zero-strict


1. c : {c:ℝ| r0 < c} 
2. n : ℤ
3. [%1] : 0 < n
4. x : ℝ^n
5. (primrec(n - 1;r0;λi,r. rmax(r;|(x i) - r0|)) < c) ⇒ (∀i:ℕn - 1. ((-(c) < (x i)) ∧ ((x i) < c)))
6. (primrec(n - 1;r0;λi,r. rmax(r;|(x i) - r0|)) < c) ⇐ ∀i:ℕn - 1. ((-(c) < (x i)) ∧ ((x i) < c))
7. ∀i:ℕn - 1. ((-(c) < (x i)) ∧ ((x i) < c))
8. -(c) < (x (n - 1))
9. (x (n - 1)) < c
10. i : ℕn
⊢ (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  <  c\} 
2.  n  :  \mBbbZ{}
3.  [\%1]  :  0  <  n
4.  x  :  \mBbbR{}\^{}n
5.  (primrec(n  -  1;r0;\mlambda{}i,r.  rmax(r;|(x  i)  -  r0|))  <  c)  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n  -  1.  ((-(c)  <  (x  i))  \mwedge{}  ((x  i)  <  c)))
6.  (primrec(n  -  1;r0;\mlambda{}i,r.  rmax(r;|(x  i)  -  r0|))  <  c)  \mLeftarrow{}{}  \mforall{}i:\mBbbN{}n  -  1.  ((-(c)  <  (x  i))  \mwedge{}  ((x  i)  <  c))
7.  \mforall{}i:\mBbbN{}n  -  1.  ((-(c)  <  (x  i))  \mwedge{}  ((x  i)  <  c))
8.  -(c)  <  (x  (n  -  1))
9.  (x  (n  -  1))  <  c
10.  i  :  \mBbbN{}n
\mvdash{}  (x  i)  <  c


By

---

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

---

Home Index