---

Step * of Lemma mdist-max-metric-ub

No Annotations
∀[n:ℕ]. ∀[x,y:ℝ^n].  ∀i:ℕn. (|(x i) - y i| ≤ mdist(max-metric(n);x;y))
BY
{ ((RepUR ``mdist max-metric`` 0 THEN InductionOnNat)
   THEN Auto
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN (OReduce 0 THENA Auto)
   THEN (BLemma `rmax_ub` THENA Auto)
   THEN Decide ⌜i < n - 1⌝⋅
   THEN Auto
   THEN Subst' i ~ n - 1 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}\^{}n].    \mforall{}i:\mBbbN{}n.  (|(x  i)  -  y  i|  \mleq{}  mdist(max-metric(n);x;y))


By

---

Latex:
((RepUR  ``mdist  max-metric``  0  THEN  InductionOnNat)
  THEN  Auto
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  (OReduce  0  THENA  Auto)
  THEN  (BLemma  `rmax\_ub`  THENA  Auto)
  THEN  Decide  \mkleeneopen{}i  <  n  -  1\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Subst'  i  \msim{}  n  -  1  0
  THEN  Auto)

---

Home Index