---

Step * of Lemma connectedness-main-lemma

No Annotations
∀x:ℝ. ∀g:ℕ ⟶ ℝ.  (lim n→∞.g n = x ⇒ (∀P:ℝ ⟶ 𝔹. ∃z:{z:ℝ| P z = P accelerate(3;x)} . (∃n:ℕ [(z = (g n))])))
BY
{ (Auto THEN (InstLemma `weak-continuity-principle-real-ext` [accelerate(3;x);⌜P⌝]⋅ THENA Auto)) }

1
1. x : ℝ
2. g : ℕ ⟶ ℝ
3. lim n→∞.g n = x
4. P : ℝ ⟶ 𝔹
5. ∀G:n:ℕ+ ⟶ {y:ℝ| accelerate(3;x) = y ∈ (ℕ+n ⟶ ℤ)} . (∃n:ℕ+ [P accelerate(3;x) = P (G n)])
⊢ ∃z:{z:ℝ| P z = P accelerate(3;x)} . (∃n:ℕ [(z = (g n))])

---

Latex:

---

Latex:
No  Annotations
\mforall{}x:\mBbbR{}.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.
    (lim  n\mrightarrow{}\minfty{}.g  n  =  x  {}\mRightarrow{}  (\mforall{}P:\mBbbR{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}z:\{z:\mBbbR{}|  P  z  =  P  accelerate(3;x)\}  .  (\mexists{}n:\mBbbN{}  [(z  =  (g  n))])))


By

---

Latex:
(Auto  THEN  (InstLemma  `weak-continuity-principle-real-ext`  [accelerate(3;x);\mkleeneopen{}P\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index