Step
*
1
1
1
2
2
1
1
2
of Lemma
cantor-to-interval-onto-proper
1. a : ℝ
2. b : ℝ
3. a < b
4. x : ℝ
5. a ≤ x
6. x ≤ b
7. ∀n:ℕ. ∀f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} .
∃g:{g:ℕn + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n + 1)), snd(cantor-interval(a;b;g;n + 1))]} . (g = f ∈ (ℕn ⟶ 𝔹)\000C)
8. g : n:ℕ
⟶ f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]}
⟶ {g:ℕn + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n + 1)), snd(cantor-interval(a;b;g;n + 1))]}
9. ∀n:ℕ. ∀f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} . ((g n f) = f ∈ (ℕn ⟶ 𝔹))
10. ∀n:ℕ. (primrec(n;λx.ff;g) ∈ {f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} )
11. λn.(primrec(n + 1;λx.ff;g) n) ∈ ℕ ⟶ 𝔹
12. n : ℕ
13. primrec(n;λx.ff;g) = primrec(n;λx.ff;g) ∈ (ℕn ⟶ 𝔹)
14. x ∈ [fst(cantor-interval(a;b;primrec(n;λx.ff;g);n)), snd(cantor-interval(a;b;primrec(n;λx.ff;g);n))]
15. x1 : ℕn
16. ∀d:ℕ. primrec(x1 + 1;λx.ff;g) x1 = primrec(x1 + d + 1;λx.ff;g) x1
⊢ primrec(x1 + 1;λx.ff;g) x1 = primrec(n;λx.ff;g) x1
BY
{ (InstHyp [⌜n - x1 + 1⌝] (-1)⋅ THENA Auto') }
1
1. a : ℝ
2. b : ℝ
3. a < b
4. x : ℝ
5. a ≤ x
6. x ≤ b
7. ∀n:ℕ. ∀f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} .
∃g:{g:ℕn + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n + 1)), snd(cantor-interval(a;b;g;n + 1))]} . (g = f ∈ (ℕn ⟶ 𝔹)\000C)
8. g : n:ℕ
⟶ f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]}
⟶ {g:ℕn + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n + 1)), snd(cantor-interval(a;b;g;n + 1))]}
9. ∀n:ℕ. ∀f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} . ((g n f) = f ∈ (ℕn ⟶ 𝔹))
10. ∀n:ℕ. (primrec(n;λx.ff;g) ∈ {f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} )
11. λn.(primrec(n + 1;λx.ff;g) n) ∈ ℕ ⟶ 𝔹
12. n : ℕ
13. primrec(n;λx.ff;g) = primrec(n;λx.ff;g) ∈ (ℕn ⟶ 𝔹)
14. x ∈ [fst(cantor-interval(a;b;primrec(n;λx.ff;g);n)), snd(cantor-interval(a;b;primrec(n;λx.ff;g);n))]
15. x1 : ℕn
16. ∀d:ℕ. primrec(x1 + 1;λx.ff;g) x1 = primrec(x1 + d + 1;λx.ff;g) x1
17. primrec(x1 + 1;λx.ff;g) x1 = primrec(x1 + (n - x1 + 1) + 1;λx.ff;g) x1
⊢ primrec(x1 + 1;λx.ff;g) x1 = primrec(n;λx.ff;g) x1
Latex:
Latex:
1. a : \mBbbR{}
2. b : \mBbbR{}
3. a < b
4. x : \mBbbR{}
5. a \mleq{} x
6. x \mleq{} b
7. \mforall{}n:\mBbbN{}. \mforall{}f:\{f:\mBbbN{}n {}\mrightarrow{} \mBbbB{}| x \mmember{} [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]\} .
\mexists{}g:\{g:\mBbbN{}n + 1 {}\mrightarrow{} \mBbbB{}| x \mmember{} [fst(cantor-interval(a;b;g;n + 1)), snd(cantor-interval(a;b;g;n + 1))]\}
(g = f)
8. g : n:\mBbbN{}
{}\mrightarrow{} f:\{f:\mBbbN{}n {}\mrightarrow{} \mBbbB{}| x \mmember{} [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]\}
{}\mrightarrow{} \{g:\mBbbN{}n + 1 {}\mrightarrow{} \mBbbB{}| x \mmember{} [fst(cantor-interval(a;b;g;n + 1)), snd(cantor-interval(a;b;g;n + 1))]\}
9. \mforall{}n:\mBbbN{}. \mforall{}f:\{f:\mBbbN{}n {}\mrightarrow{} \mBbbB{}| x \mmember{} [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]\} .
((g n f) = f)
10. \mforall{}n:\mBbbN{}
(primrec(n;\mlambda{}x.ff;g) \mmember{} \{f:\mBbbN{}n {}\mrightarrow{} \mBbbB{}|
x \mmember{} [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]\} )
11. \mlambda{}n.(primrec(n + 1;\mlambda{}x.ff;g) n) \mmember{} \mBbbN{} {}\mrightarrow{} \mBbbB{}
12. n : \mBbbN{}
13. primrec(n;\mlambda{}x.ff;g) = primrec(n;\mlambda{}x.ff;g)
14. x \mmember{} [fst(cantor-interval(a;b;primrec(n;\mlambda{}x.ff;g);n)), snd(cantor-interval(a;b;primrec(n;\mlambda{}x.ff;
g);n))]
15. x1 : \mBbbN{}n
16. \mforall{}d:\mBbbN{}. primrec(x1 + 1;\mlambda{}x.ff;g) x1 = primrec(x1 + d + 1;\mlambda{}x.ff;g) x1
\mvdash{} primrec(x1 + 1;\mlambda{}x.ff;g) x1 = primrec(n;\mlambda{}x.ff;g) x1
By
Latex:
(InstHyp [\mkleeneopen{}n - x1 + 1\mkleeneclose{}] (-1)\mcdot{} THENA Auto')
Home
Index