---

Step * of Lemma cantor-lemma2

∀z:ℕ ⟶ ℝ
  ∃f:ℕ ⟶ {p:ℝ × ℝ| (fst(p)) < (snd(p))}  ⟶ {p:ℝ × ℝ| (fst(p)) < (snd(p))} 
   ∀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)))
BY
{ (Auto
   THEN InstLemma `cantor-lemma` []
   THEN RenameVar `g' (-1)
   THEN Unfold `all` (-1)
   THEN Unfold `exists` (-1)
   THEN (InstConcl [⌜λn,p. let x,y = p in let x',y',pf = g x y (r1/r(n + 1)) (z n) in <x', y'>⌝]⋅ THENA Auto)) }

1
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)))

---

Latex:

---

Latex:
\mforall{}z:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}
    \mexists{}f:\mBbbN{}  {}\mrightarrow{}  \{p:\mBbbR{}  \mtimes{}  \mBbbR{}|  (fst(p))  <  (snd(p))\}    {}\mrightarrow{}  \{p:\mBbbR{}  \mtimes{}  \mBbbR{}|  (fst(p))  <  (snd(p))\} 
      \mforall{}n:\mBbbN{}.  \mforall{}p:\{p:\mBbbR{}  \mtimes{}  \mBbbR{}|  (fst(p))  <  (snd(p))\}  .
          let  x,y  =  p 
          in  let  x',y'  =  f  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:
(Auto
  THEN  InstLemma  `cantor-lemma`  []
  THEN  RenameVar  `g'  (-1)
  THEN  Unfold  `all`  (-1)
  THEN  Unfold  `exists`  (-1)
  THEN  (InstConcl  [\mkleeneopen{}\mlambda{}n,p.  let  x,y  =  p  in  let  x',y',pf  =  g  x  y  (r1/r(n  +  1))  (z  n)  in  <x',  y'>\mkleeneclose{}]\mcdot{}  THEN\000CA  Auto))

---

Home Index