---

Step * 2 1 1 1 1 2 of Lemma cantor-to-interval-onto-common

.....wf..... 
1. a : ℝ
2. b : ℝ
3. a < b
4. x : ℝ
5. x ∈ [a, b]
6. n : ℕ
7. f : ℕn ⟶ 𝔹
8. x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]
9. ∀n1:ℕ. ∀f1:{f:ℕn1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n1)), snd(cantor-interval(a;b;f;n1))]} .
     ∃g:{g:ℕn1 + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n1 + 1)), snd(cantor-interval(a;b;g;n1 + 1))]} 
      (g = f1 ∈ (ℕn1 ⟶ 𝔹))
10. g : n1:ℕ
⟶ f1:{f:ℕn1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n1)), snd(cantor-interval(a;b;f;n1))]} 
⟶ {g:ℕn1 + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n1 + 1)), snd(cantor-interval(a;b;g;n1 + 1))]} 
11. ∀n1:ℕ. ∀f1:{f:ℕn1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n1)), snd(cantor-interval(a;b;f;n1))]} .
      ((g n1 f1) = f1 ∈ (ℕn1 ⟶ 𝔹))
12. m : ℕ
⊢ λi,h. (g (n + i) h) ∈ ∀n@0:ℕ
                      ({f:ℕn + n@0 ⟶ 𝔹| 
                        x ∈ [fst(cantor-interval(a;b;f;n + n@0)), snd(cantor-interval(a;b;f;n + n@0))]} 
                      ⇒ {f:ℕn + n@0 + 1 ⟶ 𝔹| 
                          x ∈ [fst(cantor-interval(a;b;f;n + n@0 + 1)), snd(cantor-interval(a;b;f;n + n@0 + 1))]} )
BY
{ TACTIC:(RepeatFor 2 ((MemCD THENA Auto)) THEN Subst' n + i + 1 ~ (n + i) + 1 0 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  a  <  b
4.  x  :  \mBbbR{}
5.  x  \mmember{}  [a,  b]
6.  n  :  \mBbbN{}
7.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbB{}
8.  x  \mmember{}  [fst(cantor-interval(a;b;f;n)),  snd(cantor-interval(a;b;f;n))]
9.  \mforall{}n1:\mBbbN{}.  \mforall{}f1:\{f:\mBbbN{}n1  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;f;n1)),  snd(cantor-interval(a;b;f;n1))]\}  .
          \mexists{}g:\{g:\mBbbN{}n1  +  1  {}\mrightarrow{}  \mBbbB{}| 
                  x  \mmember{}  [fst(cantor-interval(a;b;g;n1  +  1)),  snd(cantor-interval(a;b;g;n1  +  1))]\} 
            (g  =  f1)
10.  g  :  n1:\mBbbN{}
{}\mrightarrow{}  f1:\{f:\mBbbN{}n1  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;f;n1)),  snd(cantor-interval(a;b;f;n1))]\} 
{}\mrightarrow{}  \{g:\mBbbN{}n1  +  1  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;g;n1  +  1)),  snd(cantor-interval(a;b;g;n1  +  1))]\} 
11.  \mforall{}n1:\mBbbN{}.  \mforall{}f1:\{f:\mBbbN{}n1  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;f;n1)),  snd(cantor-interval(a;b;f;n1))]\}  .
            ((g  n1  f1)  =  f1)
12.  m  :  \mBbbN{}
\mvdash{}  \mlambda{}i,h.  (g  (n  +  i)  h)  \mmember{}  \mforall{}n@0:\mBbbN{}
                                            (\{f:\mBbbN{}n  +  n@0  {}\mrightarrow{}  \mBbbB{}| 
                                                x  \mmember{}  [fst(cantor-interval(a;b;f;n  +  n@0)),  snd(cantor-interval(a;b;f;n
                                                        +  n@0))]\} 
                                            {}\mRightarrow{}  \{f:\mBbbN{}n  +  n@0  +  1  {}\mrightarrow{}  \mBbbB{}| 
                                                    x  \mmember{}  [fst(cantor-interval(a;b;f;n  +  n@0  +  1)),  snd(cantor-interval(a;b;f;n
                                                            +  n@0
                                                            +  1))]\}  )


By

---

Latex:
TACTIC:(RepeatFor  2  ((MemCD  THENA  Auto))  THEN  Subst'  n  +  i  +  1  \msim{}  (n  +  i)  +  1  0  THEN  Auto)

---

Home Index