---

Step * of Lemma max-metric_wf

∀[n:ℕ]. (max-metric(n) ∈ metric(ℝ^n))
BY
{ (Unfold `max-metric` 0
   THEN InductionOnNat
   THEN Try (((MemTypeHD (-1) THENA Auto) THEN Reduce -1))
   THEN (MemTypeCD THENW Auto)
   THEN Reduce 0
   THEN Auto
   THEN ((RWO "primrec-unroll" 0 THENA Auto) THEN Reduce 0)
   THEN (OReduce 0 THENA Auto)
   THEN Try (((RWO "-3" 0 THENA Auto) THEN nRNorm 0 THEN EAuto 1))) }

1
1. n : ℤ
2. 0 < n
3. (λp,q. primrec(n - 1;r0;λi,r. rmax(r;|(p i) - q i|)))
= (λp,q. primrec(n - 1;r0;λi,r. rmax(r;|(p i) - q i|)))
∈ (ℝ^n - 1 ⟶ ℝ^n - 1 ⟶ ℝ)
4. ∀x,y,z:ℝ^n - 1.
     (primrec(n - 1;r0;λi,r. rmax(r;|(x i) - z i|)) ≤ (primrec(n - 1;r0;λi,r. rmax(r;|(x i) - y i|))
     + primrec(n - 1;r0;λi,r. rmax(r;|(z i) - y i|))))
5. ∀x:ℝ^n - 1. (primrec(n - 1;r0;λi,r. rmax(r;|(x i) - x i|)) = r0)
6. x : ℝ^n
7. y : ℝ^n
8. z : ℝ^n
⊢ rmax(primrec(n - 1;r0;λi,r. rmax(r;|(x i) - z i|));|(x (n - 1)) - z 
                                                                (n - 1)|) ≤ (rmax(primrec(n - 1;r0;λi,r. rmax(r;|(x i) 
                                                                                                        - y i|));|(x 
                                                                                                               (n - 1)) 
- y (n - 1)|)
+ rmax(primrec(n - 1;r0;λi,r. rmax(r;|(z i) - y i|));|(z (n - 1)) - y (n - 1)|))

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  (max-metric(n)  \mmember{}  metric(\mBbbR{}\^{}n))


By

---

Latex:
(Unfold  `max-metric`  0
  THEN  InductionOnNat
  THEN  Try  (((MemTypeHD  (-1)  THENA  Auto)  THEN  Reduce  -1))
  THEN  (MemTypeCD  THENW  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  ((RWO  "primrec-unroll"  0  THENA  Auto)  THEN  Reduce  0)
  THEN  (OReduce  0  THENA  Auto)
  THEN  Try  (((RWO  "-3"  0  THENA  Auto)  THEN  nRNorm  0  THEN  EAuto  1)))

---

Home Index