---

Step * 2 1 1 1 1 1 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 : ℕ
⊢ f ∈ {f:ℕn + 0 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n + 0)), snd(cantor-interval(a;b;f;n + 0))]} 
BY
{ TACTIC:((Subst' n + 0 ~ n 0 THENA Auto) THEN MemTypeCD 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{}  f  \mmember{}  \{f:\mBbbN{}n  +  0  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;f;n  +  0)),  snd(cantor-interval(a;b;f;n  +  0))]\} 


By

---

Latex:
TACTIC:((Subst'  n  +  0  \msim{}  n  0  THENA  Auto)  THEN  MemTypeCD  THEN  Auto)

---

Home Index