---

Step * of Lemma dense-in-reals-implies-accel

∀X:ℝ ⟶ ℙ
  (dense-in-interval((-∞, ∞);X)
  ⇒ (∀x:ℝ. ∀y:{y:ℝ| y = x} .  ((X x) ⇒ (X y)))
  ⇒ (∀x:ℝ. ∀k:ℕ+.  ∃y:ℝ. ((y = accelerate(3;x) ∈ (ℕ+k ⟶ ℤ)) ∧ (X y))))
BY
{ (Auto
   THEN (RWO "dense-in-reals-iff" 2 THENA Auto)
   THEN (D 2 With ⌜x⌝  THENA Auto)
   THEN (D -1 With ⌜6 * k⌝  THENA Auto)
   THEN ExRepD) }

1
1. X : ℝ ⟶ ℙ
2. ∀x:ℝ. ∀y:{y:ℝ| y = x} .  ((X x) ⇒ (X y))
3. x : ℝ
4. k : ℕ+
5. y : ℝ
6. X y
7. |x - y| < (r1/r(6 * k))
⊢ ∃y:ℝ. ((y = accelerate(3;x) ∈ (ℕ+k ⟶ ℤ)) ∧ (X y))

---

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{}.  \mforall{}k:\mBbbN{}\msupplus{}.    \mexists{}y:\mBbbR{}.  ((y  =  accelerate(3;x))  \mwedge{}  (X  y))))


By

---

Latex:
(Auto
  THEN  (RWO  "dense-in-reals-iff"  2  THENA  Auto)
  THEN  (D  2  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}6  *  k\mkleeneclose{}    THENA  Auto)
  THEN  ExRepD)

---

Home Index