---

Step * of Lemma max-metric-sep

∀n:ℕ. ∀x,y:ℝ^n.  (r0 < mdist(max-metric(n);x;y) ⇐⇒ ∃i:ℕn. x i ≠ y i)
BY
{ (Intros
   THEN (RWO "rn-metric-sep<" 0 THENA Auto)
   THEN (InstLemma `max-metric-leq-rn-metric` [⌜n⌝]⋅ THENA Auto)
   THEN (D -1 With ⌜x⌝  THENA Auto)
   THEN (D -1 With ⌜y⌝  THENA Auto)
   THEN (InstLemma `rn-metric-leq-max-metric` [⌜n⌝]⋅ THENA Auto)
   THEN (D -1 With ⌜x⌝  THENA Auto)
   THEN (D -1 With ⌜y⌝  THENA Auto)
   THEN RepUR ``mdist scale-metric`` -1
   THEN Fold `mdist` (-1)
   THEN Auto
   THEN (CaseNat 0 `n'
         THENL [(RepUR ``mdist rn-metric`` -2 THEN Eliminate ⌜n⌝⋅ THEN RWO "real-vec-dist-dim0" (-2) THEN Auto)
               ; (nRMul ⌜r(n)⌝ 0⋅ THEN Auto)]
   )) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}x,y:\mBbbR{}\^{}n.    (r0  <  mdist(max-metric(n);x;y)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}n.  x  i  \mneq{}  y  i)


By

---

Latex:
(Intros
  THEN  (RWO  "rn-metric-sep<"  0  THENA  Auto)
  THEN  (InstLemma  `max-metric-leq-rn-metric`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}y\mkleeneclose{}    THENA  Auto)
  THEN  (InstLemma  `rn-metric-leq-max-metric`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}y\mkleeneclose{}    THENA  Auto)
  THEN  RepUR  ``mdist  scale-metric``  -1
  THEN  Fold  `mdist`  (-1)
  THEN  Auto
  THEN  (CaseNat  0  `n'
              THENL  [(RepUR  ``mdist  rn-metric``  -2
                              THEN  Eliminate  \mkleeneopen{}n\mkleeneclose{}\mcdot{}
                              THEN  RWO  "real-vec-dist-dim0"  (-2)
                              THEN  Auto)
                          ;  (nRMul  \mkleeneopen{}r(n)\mkleeneclose{}  0\mcdot{}  THEN  Auto)]
  ))

---

Home Index