---

Step * 1 1 of Lemma connectedness-main-lemma


1. x : ℝ
2. g : ℕ ⟶ ℝ
3. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|(g n) - x| ≤ (r1/r(k)))))])
4. P : ℝ ⟶ 𝔹
5. ∀G:n:ℕ+ ⟶ {y:ℝ| accelerate(3;x) = y ∈ (ℕ+n ⟶ ℤ)} . (∃n:ℕ+ [P accelerate(3;x) = P (G n)])
6. c : k:ℕ+ ⟶ ℕ
7. ∀k:ℕ+. ∀n:ℕ.  (((c k) ≤ n) ⇒ (|(g n) - x| ≤ (r1/r(k))))
8. ∀k:ℕ+. (|x - g (c k)| ≤ (r1/r(k)))
⊢ ∃z:{z:ℝ| P z = P accelerate(3;x)} . (∃n:ℕ [(z = (g n))])
BY
{ (Assert ∀k:ℕ+. (blended-real(6 * k;x;g (c (6 * k))) = accelerate(3;x) ∈ (ℕ+k ⟶ ℤ)) BY
         ((D 0 THENA Auto)
          THEN InstLemma `blended-real-agrees` [⌜6 * k⌝;⌜x⌝;⌜g (c (6 * k))⌝]⋅
          THEN Auto
          THEN (Ext THENA Auto)
          THEN RenameVar `n' (-1)
          THEN InstHyp [⌜n⌝] (-2)⋅
          THEN Auto)) }

1
1. x : ℝ
2. g : ℕ ⟶ ℝ
3. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|(g n) - x| ≤ (r1/r(k)))))])
4. P : ℝ ⟶ 𝔹
5. ∀G:n:ℕ+ ⟶ {y:ℝ| accelerate(3;x) = y ∈ (ℕ+n ⟶ ℤ)} . (∃n:ℕ+ [P accelerate(3;x) = P (G n)])
6. c : k:ℕ+ ⟶ ℕ
7. ∀k:ℕ+. ∀n:ℕ.  (((c k) ≤ n) ⇒ (|(g n) - x| ≤ (r1/r(k))))
8. ∀k:ℕ+. (|x - g (c k)| ≤ (r1/r(k)))
9. ∀k:ℕ+. (blended-real(6 * k;x;g (c (6 * k))) = accelerate(3;x) ∈ (ℕ+k ⟶ ℤ))
⊢ ∃z:{z:ℝ| P z = P accelerate(3;x)} . (∃n:ℕ [(z = (g n))])

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  g  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
3.  \mforall{}k:\mBbbN{}\msupplus{}.  (\mexists{}N:\mBbbN{}  [(\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  (|(g  n)  -  x|  \mleq{}  (r1/r(k)))))])
4.  P  :  \mBbbR{}  {}\mrightarrow{}  \mBbbB{}
5.  \mforall{}G:n:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \{y:\mBbbR{}|  accelerate(3;x)  =  y\}  .  (\mexists{}n:\mBbbN{}\msupplus{}  [P  accelerate(3;x)  =  P  (G  n)])
6.  c  :  k:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbN{}
7.  \mforall{}k:\mBbbN{}\msupplus{}.  \mforall{}n:\mBbbN{}.    (((c  k)  \mleq{}  n)  {}\mRightarrow{}  (|(g  n)  -  x|  \mleq{}  (r1/r(k))))
8.  \mforall{}k:\mBbbN{}\msupplus{}.  (|x  -  g  (c  k)|  \mleq{}  (r1/r(k)))
\mvdash{}  \mexists{}z:\{z:\mBbbR{}|  P  z  =  P  accelerate(3;x)\}  .  (\mexists{}n:\mBbbN{}  [(z  =  (g  n))])


By

---

Latex:
(Assert  \mforall{}k:\mBbbN{}\msupplus{}.  (blended-real(6  *  k;x;g  (c  (6  *  k)))  =  accelerate(3;x))  BY
              ((D  0  THENA  Auto)
                THEN  InstLemma  `blended-real-agrees`  [\mkleeneopen{}6  *  k\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}g  (c  (6  *  k))\mkleeneclose{}]\mcdot{}
                THEN  Auto
                THEN  (Ext  THENA  Auto)
                THEN  RenameVar  `n'  (-1)
                THEN  InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-2)\mcdot{}
                THEN  Auto))

---

Home Index