---

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

No Annotations
∀c:{c:ℝ| r0 < c} . ∀n:ℕ. ∀x:ℝ^n.  ((∀i:ℕn. (|x i| < c)) ⇒ (mdist(max-metric(n);x;λi.r0) < c))
BY
{ (Auto THEN BLemma `mdist-max-metric-strict-lb` THEN Reduce 0 THEN Auto THEN nRNorm 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  BLemma  `mdist-max-metric-strict-lb`  THEN  Reduce  0  THEN  Auto  THEN  nRNorm  0  THEN  Auto)

---

Home Index