---

Step * of Lemma dense-in-reals-iff

∀X:ℝ ⟶ ℙ. (dense-in-interval((-∞, ∞);X) ⇐⇒ ∀x:ℝ. ∀n:ℕ+.  ∃y:ℝ. ((X y) ∧ (|x - y| < (r1/r(n)))))
BY
{ Auto }

1
1. X : ℝ ⟶ ℙ
2. dense-in-interval((-∞, ∞);X)
3. x : ℝ
4. n : ℕ+
⊢ ∃y:ℝ. ((X y) ∧ (|x - y| < (r1/r(n))))

2
1. X : ℝ ⟶ ℙ
2. ∀x:ℝ. ∀n:ℕ+.  ∃y:ℝ. ((X y) ∧ (|x - y| < (r1/r(n))))
⊢ dense-in-interval((-∞, ∞);X)

---

Latex:

---

Latex:
\mforall{}X:\mBbbR{}  {}\mrightarrow{}  \mBbbP{}.  (dense-in-interval((-\minfty{},  \minfty{});X)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    \mexists{}y:\mBbbR{}.  ((X  y)  \mwedge{}  (|x  -  y|  <  (r1/r(n)))))


By

---

Latex:
Auto

---

Home Index