---

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

∀[c:{c:ℝ| r0 ≤ c} ]. ∀[n:ℕ]. ∀[x:ℝ^n].  uiff(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 (RWO "rmax_lb<" 0⋅ THENA Auto)
           THEN (RWO "-1" 0 THENA Auto)
           THEN RWO "rabs-difference-bound-rleq" 0
           THEN Auto)
   )) }

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

2
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

3
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))

4
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))
⊢ (x (n - 1)) ≤ (r0 + c)

---

Latex:

---

Latex:
\mforall{}[c:\{c:\mBbbR{}|  r0  \mleq{}  c\}  ].  \mforall{}[n:\mBbbN{}].  \mforall{}[x:\mBbbR{}\^{}n].
    uiff(mdist(max-metric(n);x;\mlambda{}i.r0)  \mleq{}  c;\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  (RWO  "rmax\_lb<"  0\mcdot{}  THENA  Auto)
                  THEN  (RWO  "-1"  0  THENA  Auto)
                  THEN  RWO  "rabs-difference-bound-rleq"  0
                  THEN  Auto)
  ))

---

Home Index