---

Step * of Lemma dense-in-reals-implies

∀X:ℝ ⟶ ℙ
  (dense-in-interval((-∞, ∞);X)
  ⇒ (∀x:ℝ. ∀y:{y:ℝ| y = x} .  ((X x) ⇒ (X y)))
  ⇒ (∀x:ℝ. ∃x':ℝ. ((x' = x) ∧ (∀k:ℕ+. ∃y:ℝ. ((y = x' ∈ (ℕ+k ⟶ ℤ)) ∧ (X y))))))
BY
{ (InstLemma `dense-in-reals-implies-accel` []
   THEN RepeatFor 4 ((ParallelLast' THENA Auto))
   THEN D 0 With ⌜accelerate(3;x)⌝ 
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}X:\mBbbR{}  {}\mrightarrow{}  \mBbbP{}
    (dense-in-interval((-\minfty{},  \minfty{});X)
    {}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  \mforall{}y:\{y:\mBbbR{}|  y  =  x\}  .    ((X  x)  {}\mRightarrow{}  (X  y)))
    {}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  \mexists{}x':\mBbbR{}.  ((x'  =  x)  \mwedge{}  (\mforall{}k:\mBbbN{}\msupplus{}.  \mexists{}y:\mBbbR{}.  ((y  =  x')  \mwedge{}  (X  y))))))


By

---

Latex:
(InstLemma  `dense-in-reals-implies-accel`  []
  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto))
  THEN  D  0  With  \mkleeneopen{}accelerate(3;x)\mkleeneclose{} 
  THEN  Auto)

---

Home Index