---

Step * of Lemma approx-fixpoint

∀I:{I:Interval| icompact(I)} . ∀n:ℕ. ∀f:{f:I^n ⟶ I^n| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ req-vec(n;f a;f b))} .
  ((¬(∀x:I^n. f x ≠ x)) ⇒ (∀e:{e:ℝ| r0 < e} . ∃x:I^n. (d(f x;x) < e)))
BY
{ (InstLemma `approx-zero` []
   THEN RepeatFor 2 (ParallelLast')
   THEN Auto
   THEN (InstHyp [⌜λx.d(f x;x)⌝;⌜e⌝] 3⋅ THEN All Reduce)
   THEN Auto) }

1
1. I : {I:Interval| icompact(I)} 
2. n : ℕ
3. ∀f:{f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))} 
     ((¬(∀x:I^n. f x ≠ r0)) ⇒ (∀e:{e:ℝ| r0 < e} . ∃x:I^n. (|f x| < e)))
4. f : {f:I^n ⟶ I^n| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ req-vec(n;f a;f b))} 
5. ¬(∀x:I^n. f x ≠ x)
6. e : {e:ℝ| r0 < e} 
⊢ λx.d(f x;x) ∈ {f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))} 

2
1. I : {I:Interval| icompact(I)} 
2. n : ℕ
3. ∀f:{f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))} 
     ((¬(∀x:I^n. f x ≠ r0)) ⇒ (∀e:{e:ℝ| r0 < e} . ∃x:I^n. (|f x| < e)))
4. f : {f:I^n ⟶ I^n| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ req-vec(n;f a;f b))} 
5. ¬(∀x:I^n. f x ≠ x)
6. e : {e:ℝ| r0 < e} 
⊢ ¬(∀x:I^n. d(f x;x) ≠ r0)

3
1. I : {I:Interval| icompact(I)} 
2. n : ℕ
3. ∀f:{f:I^n ⟶ ℝ| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ ((f a) = (f b)))} 
     ((¬(∀x:I^n. f x ≠ r0)) ⇒ (∀e:{e:ℝ| r0 < e} . ∃x:I^n. (|f x| < e)))
4. f : {f:I^n ⟶ I^n| ∀a,b:I^n.  (req-vec(n;a;b) ⇒ req-vec(n;f a;f b))} 
5. ¬(∀x:I^n. f x ≠ x)
6. e : {e:ℝ| r0 < e} 
7. ∃x:I^n. (|d(f x;x)| < e)
⊢ ∃x:I^n. (d(f x;x) < e)

---

Latex:

---

Latex:
\mforall{}I:\{I:Interval|  icompact(I)\}  .  \mforall{}n:\mBbbN{}.  \mforall{}f:\{f:I\^{}n  {}\mrightarrow{}  I\^{}n| 
                                                                                \mforall{}a,b:I\^{}n.    (req-vec(n;a;b)  {}\mRightarrow{}  req-vec(n;f  a;f  b))\}  .
    ((\mneg{}(\mforall{}x:I\^{}n.  f  x  \mneq{}  x))  {}\mRightarrow{}  (\mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .  \mexists{}x:I\^{}n.  (d(f  x;x)  <  e)))


By

---

Latex:
(InstLemma  `approx-zero`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}x.d(f  x;x)\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  3\mcdot{}  THEN  All  Reduce)
  THEN  Auto)

---

Home Index