---

Step * of Lemma mdist-max-metric-strict-lb

No Annotations
∀c:{c:ℝ| r0 < c} . ∀n:ℕ. ∀x,y:ℝ^n.  ((∀i:ℕn. (|(x i) - y i| < c)) ⇒ (mdist(max-metric(n);x;y) < c))
BY
{ ((RepUR ``mdist max-metric`` 0 THEN InductionOnNat)
   THEN Auto
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN (OReduce 0 THENA Auto)
   THEN Try (BLemma `rmax_strict_lb`)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((RepUR  ``mdist  max-metric``  0  THEN  InductionOnNat)
  THEN  Auto
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  (OReduce  0  THENA  Auto)
  THEN  Try  (BLemma  `rmax\_strict\_lb`)
  THEN  Auto)

---

Home Index