Step
*
2
1
1
1
1
of Lemma
cantor-to-interval-onto-common
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 ⟶ 𝔹))
⊢ ∃g:ℕ ⟶ 𝔹. ((cantor-to-interval(a;b;g) = x) ∧ (g = f ∈ (ℕn ⟶ 𝔹)))
BY
{ (Assert ⌜∀m:ℕ
(primrec(m;f;λi,h. (g (n + i) h)) ∈ {f:ℕn + m ⟶ 𝔹|
x ∈ [fst(cantor-interval(a;b;f;n + m)), snd(cantor-interval(a;b;f;n
+ m))]} )⌝⋅
THENA ((D 0 THENA Auto)
THEN InstLemma `primrec-wf` [⌜λ2m.{f:ℕn + m ⟶ 𝔹|
x ∈ [fst(cantor-interval(a;b;f;n + m)), snd(cantor-interval(a;b;f;n
+ m))]} ⌝
; ⌜f⌝;⌜λi,h. (g (n + i) h)⌝;⌜m⌝]⋅
THEN Try (QuickAuto))
) }
1
.....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))]}
2
.....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))]} )
3
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:ℕ
(primrec(m;f;λi,h. (g (n + i) h)) ∈ {f:ℕn + m ⟶ 𝔹|
x ∈ [fst(cantor-interval(a;b;f;n + m)), snd(cantor-interval(a;b;f;n + m))]} )
⊢ ∃g:ℕ ⟶ 𝔹. ((cantor-to-interval(a;b;g) = x) ∧ (g = f ∈ (ℕn ⟶ 𝔹)))
Latex:
Latex:
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)
\mvdash{} \mexists{}g:\mBbbN{} {}\mrightarrow{} \mBbbB{}. ((cantor-to-interval(a;b;g) = x) \mwedge{} (g = f))
By
Latex:
(Assert \mkleeneopen{}\mforall{}m:\mBbbN{}
(primrec(m;f;\mlambda{}i,h. (g (n + i) h)) \mmember{} \{f:\mBbbN{}n + m {}\mrightarrow{} \mBbbB{}|
x \mmember{} [fst(cantor-interval(a;b;f;n
+ m)), snd(cantor-interval(a;b;f;n + m))]\} )\mkleeneclose{}\mcdot{}
THENA ((D 0 THENA Auto)
THEN InstLemma `primrec-wf` [\mkleeneopen{}\mlambda{}\msubtwo{}m.\{f:\mBbbN{}n + m {}\mrightarrow{} \mBbbB{}|
x \mmember{} [fst(cantor-interval(a;b;f;n
+ m)), snd(cantor-interval(a;b;f;n + m))]\} \mkleeneclose{}
; \mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}\mlambda{}i,h. (g (n + i) h)\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}
THEN Try (QuickAuto))
)
Home
Index