---

Step * of Lemma approx-fixpoint-unit-ball-0

∀n:ℕ+. ∀f:{f:B(n) ⟶ B(n)| 
           (∀e:{e:ℝ| r0 < e} . ∃del:{del:ℝ| r0 < del} . ∀x,y:B(n).  ((d(x;y) < del) ⇒ (d(f x;f y) < e)))
           ∧ (¬(∀x:B(n). f x ≠ x))} . ∀e:{e:ℝ| r0 < e} .
  ∃t:B(n) ⟶ 𝔹
   ((∀p:B(n). ((↑(t p)) ⇒ (↓d(f p;p) < e))) ∧ (↓∃k:ℕ+. ∃q:unit-ball-approx(n;k). (↑(t approx-ball-to-ball(k;q)))))
BY
{ (Auto
   THEN (Assert r0 < (e/r(3)) BY
               (nRMul ⌜r(3)⌝ 0⋅ THEN Auto))
   THEN (Assert ∀p:B(n). (((r(2) * e/r(3)) < d(f p;p)) ∨ (d(f p;p) < e)) BY
               (Auto
                THEN (BLemma `rless-cases` THEN Auto)
                THEN nRMul ⌜r(3)⌝ 0⋅
                THEN Auto
                THEN nRAdd ⌜r(-2) * e⌝ 0⋅
                THEN Auto))
   THEN RenameVar `t' (-1)
   THEN (Assert ∀p:B(n). ((↑isr(t p)) ⇒ (d(f p;p) < e)) BY
               ((D 0 THENA Auto) THEN (GenConclTerm ⌜t p⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0 THEN Auto))
   THEN (Assert ∀p:B(n). ((¬↑isr(t p)) ⇒ ((r(2) * e/r(3)) < d(f p;p))) BY
               ((D 0 THENA Auto) THEN (GenConclTerm ⌜t p⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0 THEN Auto))
   THEN (D 0 With ⌜λp.isr(t p)⌝  THENA Auto)
   THEN Reduce 0
   THEN D 0
   THEN Try ((Trivial ORELSE Complete ((ParallelOp -2 THEN ParallelLast))))) }

1
1. n : ℕ+
2. f : {f:B(n) ⟶ B(n)| 
        (∀e:{e:ℝ| r0 < e} . ∃del:{del:ℝ| r0 < del} . ∀x,y:B(n).  ((d(x;y) < del) ⇒ (d(f x;f y) < e)))
        ∧ (¬(∀x:B(n). f x ≠ x))} 
3. e : {e:ℝ| r0 < e} 
4. r0 < (e/r(3))
5. t : ∀p:B(n). (((r(2) * e/r(3)) < d(f p;p)) ∨ (d(f p;p) < e))
6. ∀p:B(n). ((↑isr(t p)) ⇒ (d(f p;p) < e))
7. ∀p:B(n). ((¬↑isr(t p)) ⇒ ((r(2) * e/r(3)) < d(f p;p)))
⊢ ↓∃k:ℕ+. ∃q:unit-ball-approx(n;k). (↑isr(t approx-ball-to-ball(k;q)))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}f:\{f:B(n)  {}\mrightarrow{}  B(n)| 
                      (\mforall{}e:\{e:\mBbbR{}|  r0  <  e\} 
                            \mexists{}del:\{del:\mBbbR{}|  r0  <  del\}  .  \mforall{}x,y:B(n).    ((d(x;y)  <  del)  {}\mRightarrow{}  (d(f  x;f  y)  <  e)))
                      \mwedge{}  (\mneg{}(\mforall{}x:B(n).  f  x  \mneq{}  x))\}  .  \mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .
    \mexists{}t:B(n)  {}\mrightarrow{}  \mBbbB{}
      ((\mforall{}p:B(n).  ((\muparrow{}(t  p))  {}\mRightarrow{}  (\mdownarrow{}d(f  p;p)  <  e)))
      \mwedge{}  (\mdownarrow{}\mexists{}k:\mBbbN{}\msupplus{}.  \mexists{}q:unit-ball-approx(n;k).  (\muparrow{}(t  approx-ball-to-ball(k;q)))))


By

---

Latex:
(Auto
  THEN  (Assert  r0  <  (e/r(3))  BY
                          (nRMul  \mkleeneopen{}r(3)\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  (Assert  \mforall{}p:B(n).  (((r(2)  *  e/r(3))  <  d(f  p;p))  \mvee{}  (d(f  p;p)  <  e))  BY
                          (Auto
                            THEN  (BLemma  `rless-cases`  THEN  Auto)
                            THEN  nRMul  \mkleeneopen{}r(3)\mkleeneclose{}  0\mcdot{}
                            THEN  Auto
                            THEN  nRAdd  \mkleeneopen{}r(-2)  *  e\mkleeneclose{}  0\mcdot{}
                            THEN  Auto))
  THEN  RenameVar  `t'  (-1)
  THEN  (Assert  \mforall{}p:B(n).  ((\muparrow{}isr(t  p))  {}\mRightarrow{}  (d(f  p;p)  <  e))  BY
                          ((D  0  THENA  Auto)
                            THEN  (GenConclTerm  \mkleeneopen{}t  p\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  D  -2
                            THEN  Reduce  0
                            THEN  Auto))
  THEN  (Assert  \mforall{}p:B(n).  ((\mneg{}\muparrow{}isr(t  p))  {}\mRightarrow{}  ((r(2)  *  e/r(3))  <  d(f  p;p)))  BY
                          ((D  0  THENA  Auto)
                            THEN  (GenConclTerm  \mkleeneopen{}t  p\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  D  -2
                            THEN  Reduce  0
                            THEN  Auto))
  THEN  (D  0  With  \mkleeneopen{}\mlambda{}p.isr(t  p)\mkleeneclose{}    THENA  Auto)
  THEN  Reduce  0
  THEN  D  0
  THEN  Try  ((Trivial  ORELSE  Complete  ((ParallelOp  -2  THEN  ParallelLast)))))

---

Home Index