---

Step * of Lemma rationals-dense-in-interval

∀I:Interval. dense-in-interval(I;λr.∃z:ℤ. ∃d:ℕ+. (r = (r(z)/r(d))))
BY
{ (Auto THEN (D 0 THEN Auto) THEN Reduce 0) }

1
1. I : Interval
2. a : {a:ℝ| a ∈ I} 
3. b : {r:ℝ| r ∈ I} 
4. a < b
⊢ ∃x:ℝ. ((∃z:ℤ. ∃d:ℕ+. (x = (r(z)/r(d)))) ∧ (a < x) ∧ (x < b))

---

Latex:

---

Latex:
\mforall{}I:Interval.  dense-in-interval(I;\mlambda{}r.\mexists{}z:\mBbbZ{}.  \mexists{}d:\mBbbN{}\msupplus{}.  (r  =  (r(z)/r(d))))


By

---

Latex:
(Auto  THEN  (D  0  THEN  Auto)  THEN  Reduce  0)

---

Home Index