---

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

No Annotations
∀c:{c:ℝ| r0 < c} . ∀n:ℕ. ∀x:ℝ^n.  (mdist(max-metric(n);x;λi.r0) < c ⇐⇒ ∀i:ℕn. (x i ∈ (-(c), c)))
BY
{ (RepUR ``mdist max-metric`` 0
   THEN InductionOnNat
   THEN Reduce 0
   THEN (Complete (Auto)
   ORELSE ((D 0 THENA Auto)
           THEN (D -2 With ⌜x⌝  THENA Auto)
           THEN (RWO "primrec-unroll" 0 THENA Auto)
           THEN Reduce 0
           THEN (OReduce 0 THENA Auto)
           THEN (RWW "rmax_strict_lb< -1" 0⋅ THENA Auto)
           THEN (nRNorm 0 THENA Auto)
           THEN RWO "rabs-rless-iff" 0
           THEN Auto)
   )) }

1
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
⊢ -(c) < (x i)

2
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

---

Latex:

---

Latex:
No  Annotations
\mforall{}c:\{c:\mBbbR{}|  r0  <  c\}  .  \mforall{}n:\mBbbN{}.  \mforall{}x:\mBbbR{}\^{}n.    (mdist(max-metric(n);x;\mlambda{}i.r0)  <  c  \mLeftarrow{}{}\mRightarrow{}  \mforall{}i:\mBbbN{}n.  (x  i  \mmember{}  (-(c),  c)))


By

---

Latex:
(RepUR  ``mdist  max-metric``  0
  THEN  InductionOnNat
  THEN  Reduce  0
  THEN  (Complete  (Auto)
  ORELSE  ((D  0  THENA  Auto)
                  THEN  (D  -2  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto)
                  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
                  THEN  Reduce  0
                  THEN  (OReduce  0  THENA  Auto)
                  THEN  (RWW  "rmax\_strict\_lb<  -1"  0\mcdot{}  THENA  Auto)
                  THEN  (nRNorm  0  THENA  Auto)
                  THEN  RWO  "rabs-rless-iff"  0
                  THEN  Auto)
  ))

---

Home Index