---

Step * 1 of Lemma rationals-dense-in-interval


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))
BY
{ ((InstLemma `rationals-dense` [⌜a⌝;⌜b⌝]⋅ THENA Auto) THEN ExRepD THEN D 0 With ⌜(r(m)/r(n))⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  a  :  \{a:\mBbbR{}|  a  \mmember{}  I\} 
3.  b  :  \{r:\mBbbR{}|  r  \mmember{}  I\} 
4.  a  <  b
\mvdash{}  \mexists{}x:\mBbbR{}.  ((\mexists{}z:\mBbbZ{}.  \mexists{}d:\mBbbN{}\msupplus{}.  (x  =  (r(z)/r(d))))  \mwedge{}  (a  <  x)  \mwedge{}  (x  <  b))


By

---

Latex:
((InstLemma  `rationals-dense`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  D  0  With  \mkleeneopen{}(r(m)/r(n))\mkleeneclose{} 
  THEN  Auto)

---

Home Index