---

Step * of Lemma realvec-max-ibs-property

∀k:ℕ. ∀p:ℝ^k.
  ((r0 < mdist(max-metric(k);p;λi.r0) ⇐⇒ ∃n:ℕ. ((realvec-max-ibs(k;p) n) = 1 ∈ ℤ))
  ∧ (∀n:ℕ. (((realvec-max-ibs(k;p) n) = 0 ∈ ℤ) ⇒ (mdist(max-metric(k);p;λi.r0) ≤ (r(4)/r(n + 1))))))
BY
{ (((Intros THEN (Assert λi.r0 ∈ ℝ^k BY Auto))
    THEN (Assert r0 ≤ mdist(max-metric(k);p;λi.r0) BY
                Auto)
    THEN (Assert |r0 - mdist(max-metric(k);p;λi.r0)| = mdist(max-metric(k);p;λi.r0) BY
                (nRNorm 0
                 THEN RWO "rabs-rminus" 0
                 THEN InstLemma `rabs-of-nonneg` [⌜mdist(max-metric(k);p;λi.r0)⌝]⋅
                 THEN Auto)))
   THEN Unfold `realvec-max-ibs` 0
   THEN (InstLemma `rless_ibs_property` [⌜r0⌝;⌜mdist(max-metric(k);p;λi.r0)⌝]⋅ THENA Auto)
   THEN RepeatFor 3 (ParallelLast)
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}p:\mBbbR{}\^{}k.
    ((r0  <  mdist(max-metric(k);p;\mlambda{}i.r0)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  ((realvec-max-ibs(k;p)  n)  =  1))
    \mwedge{}  (\mforall{}n:\mBbbN{}.  (((realvec-max-ibs(k;p)  n)  =  0)  {}\mRightarrow{}  (mdist(max-metric(k);p;\mlambda{}i.r0)  \mleq{}  (r(4)/r(n  +  1))))))


By

---

Latex:
(((Intros  THEN  (Assert  \mlambda{}i.r0  \mmember{}  \mBbbR{}\^{}k  BY  Auto))
    THEN  (Assert  r0  \mleq{}  mdist(max-metric(k);p;\mlambda{}i.r0)  BY
                            Auto)
    THEN  (Assert  |r0  -  mdist(max-metric(k);p;\mlambda{}i.r0)|  =  mdist(max-metric(k);p;\mlambda{}i.r0)  BY
                            (nRNorm  0
                              THEN  RWO  "rabs-rminus"  0
                              THEN  InstLemma  `rabs-of-nonneg`  [\mkleeneopen{}mdist(max-metric(k);p;\mlambda{}i.r0)\mkleeneclose{}]\mcdot{}
                              THEN  Auto)))
  THEN  Unfold  `realvec-max-ibs`  0
  THEN  (InstLemma  `rless\_ibs\_property`  [\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}mdist(max-metric(k);p;\mlambda{}i.r0)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  3  (ParallelLast)
  THEN  D  -1
  THEN  Auto)

---

Home Index