---

Step * 1 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)))
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))])
BY
{ ((InstHyp [⌜λk.blended-real(6 * k;x;g (c (6 * k)))⌝] 5⋅ THENA (Auto THEN MemTypeCD THEN Auto)) THEN Reduce -1) }

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 ⟶ ℤ))
10. ∃n:ℕ+ [P accelerate(3;x) = P blended-real(6 * n;x;g (c (6 * n)))]
⊢ ∃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)))
9.  \mforall{}k:\mBbbN{}\msupplus{}.  (blended-real(6  *  k;x;g  (c  (6  *  k)))  =  accelerate(3;x))
\mvdash{}  \mexists{}z:\{z:\mBbbR{}|  P  z  =  P  accelerate(3;x)\}  .  (\mexists{}n:\mBbbN{}  [(z  =  (g  n))])


By

---

Latex:
((InstHyp  [\mkleeneopen{}\mlambda{}k.blended-real(6  *  k;x;g  (c  (6  *  k)))\mkleeneclose{}]  5\mcdot{}  THENA  (Auto  THEN  MemTypeCD  THEN  Auto))
  THEN  Reduce  -1
  )

---

Home Index