---

Step * of Lemma remove-singularity-max-seq_wf

∀[X:Type]. ∀[k:ℕ]. ∀[p:ℝ^k]. ∀[f:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)}  ⟶ X]. ∀[z:X].
  (remove-singularity-max-seq(k;p;f;z) ∈ ℕ ⟶ X)
BY
{ (RepeatFor 3 (Intro)
   THEN (Assert λi.r0 ∈ ℝ^k BY
               Auto)
   THEN ProveWfLemma
   THEN InstLemma `realvec-max-ibs-property` [⌜k⌝;⌜p⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[k:\mBbbN{}].  \mforall{}[p:\mBbbR{}\^{}k].  \mforall{}[f:\{p:\mBbbR{}\^{}k|  r0  <  mdist(max-metric(k);p;\mlambda{}i.r0)\}    {}\mrightarrow{}  X].  \mforall{}[z:X].
    (remove-singularity-max-seq(k;p;f;z)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  X)


By

---

Latex:
(RepeatFor  3  (Intro)
  THEN  (Assert  \mlambda{}i.r0  \mmember{}  \mBbbR{}\^{}k  BY
                          Auto)
  THEN  ProveWfLemma
  THEN  InstLemma  `realvec-max-ibs-property`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index