---

Step * 1 of Lemma cantor-lemma2


1. z : ℕ ⟶ ℝ
2. g : x:ℝ
⟶ y:ℝ
⟶ e:ℝ
⟶ z:ℝ
⟶ (x':ℝ × y':ℝ × ((x ≤ x') ∧ (x' < y') ∧ (y' ≤ y) ∧ ((z < x') ∨ (y' < z)) ∧ ((y' - x') < e))) supposing 
      ((x < y) and 
      (r0 < e))
⊢ ∀n:ℕ. ∀p:{p:ℝ × ℝ| (fst(p)) < (snd(p))} .
    let x,y = p 
    in let x',y' = (λn,p. let x,y = p in let x',y',pf = g x y (r1/r(n + 1)) (z n) in <x', y'>) n p 
       in (x ≤ x') ∧ (x' < y') ∧ (y' ≤ y) ∧ (((z n) < x') ∨ (y' < (z n))) ∧ ((y' - x') < (r1/r(n + 1)))
BY
{ (Reduce 0
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN RepeatFor 2 (DVar `p')
   THEN All Reduce
   THEN (Assert p1 < p2 BY
               (Unhide THEN Auto))
   THEN (GenConclAtAddrType ⌜x':ℝ
                             × y':ℝ
                             × ((p1 ≤ x')
                               ∧ (x' < y')
                               ∧ (y' ≤ p2)
                               ∧ (((z n) < x') ∨ (y' < (z n)))
                               ∧ ((y' - x') < (r1/r(n + 1))))⌝ [1;1]⋅
         THEN Auto
         THEN (RepeatFor 2 (D (-2)) THEN Reduce 0 THEN Auto)⋅)⋅)⋅ }

---

Latex:

---

Latex:

1.  z  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  g  :  x:\mBbbR{}
{}\mrightarrow{}  y:\mBbbR{}
{}\mrightarrow{}  e:\mBbbR{}
{}\mrightarrow{}  z:\mBbbR{}
{}\mrightarrow{}  (x':\mBbbR{}
            \mtimes{}  y':\mBbbR{}
            \mtimes{}  ((x  \mleq{}  x')  \mwedge{}  (x'  <  y')  \mwedge{}  (y'  \mleq{}  y)  \mwedge{}  ((z  <  x')  \mvee{}  (y'  <  z))  \mwedge{}  ((y'  -  x')  <  e)))  supposing 
            ((x  <  y)  and 
            (r0  <  e))
\mvdash{}  \mforall{}n:\mBbbN{}.  \mforall{}p:\{p:\mBbbR{}  \mtimes{}  \mBbbR{}|  (fst(p))  <  (snd(p))\}  .
        let  x,y  =  p 
        in  let  x',y'  =  (\mlambda{}n,p.  let  x,y  =  p  in  let  x',y',pf  =  g  x  y  (r1/r(n  +  1))  (z  n)  in  <x',  y'>)  n  p 
              in  (x  \mleq{}  x')
                    \mwedge{}  (x'  <  y')
                    \mwedge{}  (y'  \mleq{}  y)
                    \mwedge{}  (((z  n)  <  x')  \mvee{}  (y'  <  (z  n)))
                    \mwedge{}  ((y'  -  x')  <  (r1/r(n  +  1)))


By

---

Latex:
(Reduce  0
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RepeatFor  2  (DVar  `p')
  THEN  All  Reduce
  THEN  (Assert  p1  <  p2  BY
                          (Unhide  THEN  Auto))
  THEN  (GenConclAtAddrType  \mkleeneopen{}x':\mBbbR{}
                                                      \mtimes{}  y':\mBbbR{}
                                                      \mtimes{}  ((p1  \mleq{}  x')
                                                          \mwedge{}  (x'  <  y')
                                                          \mwedge{}  (y'  \mleq{}  p2)
                                                          \mwedge{}  (((z  n)  <  x')  \mvee{}  (y'  <  (z  n)))
                                                          \mwedge{}  ((y'  -  x')  <  (r1/r(n  +  1))))\mkleeneclose{}  [1;1]\mcdot{}
              THEN  Auto
              THEN  (RepeatFor  2  (D  (-2))  THEN  Reduce  0  THEN  Auto)\mcdot{})\mcdot{})\mcdot{}

---

Home Index