---

Step * of Lemma reals-uncountable

∀z:ℕ ⟶ ℝ. ∀x,y:ℝ.  ((x < y) ⇒ (∃u:ℝ. ((x ≤ u) ∧ (u ≤ y) ∧ (∀n:ℕ. u ≠ z n))))
BY
{ (Auto
   THEN ((InstLemma `cantor-lemma2` [⌜z⌝])⋅ THENA Auto)
   THEN ExRepD
   THEN (Assert ∀n:ℕ. (primrec(n;<x, y>;f) ∈ {p:ℝ × ℝ| (fst(p)) < (snd(p))} ) BY
               (Auto THEN Auto THEN Reduce 0 THEN Auto))) }

1
1. z : ℕ ⟶ ℝ
2. x : ℝ
3. y : ℝ
4. x < y
5. f : ℕ ⟶ {p:ℝ × ℝ| (fst(p)) < (snd(p))}  ⟶ {p:ℝ × ℝ| (fst(p)) < (snd(p))} 
6. ∀n:ℕ. ∀p:{p:ℝ × ℝ| (fst(p)) < (snd(p))} .
     let x,y = p 
     in let x',y' = f n p 
        in (x ≤ x') ∧ (x' < y') ∧ (y' ≤ y) ∧ (((z n) < x') ∨ (y' < (z n))) ∧ ((y' - x') < (r1/r(n + 1)))
7. ∀n:ℕ. (primrec(n;<x, y>;f) ∈ {p:ℝ × ℝ| (fst(p)) < (snd(p))} )
⊢ ∃u:ℝ. ((x ≤ u) ∧ (u ≤ y) ∧ (∀n:ℕ. u ≠ z n))

---

Latex:

---

Latex:
\mforall{}z:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}x,y:\mBbbR{}.    ((x  <  y)  {}\mRightarrow{}  (\mexists{}u:\mBbbR{}.  ((x  \mleq{}  u)  \mwedge{}  (u  \mleq{}  y)  \mwedge{}  (\mforall{}n:\mBbbN{}.  u  \mneq{}  z  n))))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `cantor-lemma2`  [\mkleeneopen{}z\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (Assert  \mforall{}n:\mBbbN{}.  (primrec(n;<x,  y>f)  \mmember{}  \{p:\mBbbR{}  \mtimes{}  \mBbbR{}|  (fst(p))  <  (snd(p))\}  )  BY
                          (Auto  THEN  Auto  THEN  Reduce  0  THEN  Auto)))

---

Home Index