Step
*
1
of Lemma
cantor-to-int-bounded
1. F : (ℕ ⟶ 𝔹) ⟶ ℤ
2. n : ℕ
3. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹))
⇒ ((F f) = (F g) ∈ ℤ))
⊢ ∃B:ℕ. ∀f:ℕ ⟶ 𝔹. (|F f| ≤ B)
BY
{ Assert ⌜∃B:ℕ. ∀s:ℕn ⟶ 𝔹. (|F (λi.if i <z n then s i else ff fi )| ≤ B)⌝⋅ }
1
.....assertion.....
1. F : (ℕ ⟶ 𝔹) ⟶ ℤ
2. n : ℕ
3. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹))
⇒ ((F f) = (F g) ∈ ℤ))
⊢ ∃B:ℕ. ∀s:ℕn ⟶ 𝔹. (|F (λi.if i <z n then s i else ff fi )| ≤ B)
2
1. F : (ℕ ⟶ 𝔹) ⟶ ℤ
2. n : ℕ
3. ∀f,g:ℕ ⟶ 𝔹. ((f = g ∈ (ℕn ⟶ 𝔹))
⇒ ((F f) = (F g) ∈ ℤ))
4. ∃B:ℕ. ∀s:ℕn ⟶ 𝔹. (|F (λi.if i <z n then s i else ff fi )| ≤ B)
⊢ ∃B:ℕ. ∀f:ℕ ⟶ 𝔹. (|F f| ≤ B)
Latex:
Latex:
1. F : (\mBbbN{} {}\mrightarrow{} \mBbbB{}) {}\mrightarrow{} \mBbbZ{}
2. n : \mBbbN{}
3. \mforall{}f,g:\mBbbN{} {}\mrightarrow{} \mBbbB{}. ((f = g) {}\mRightarrow{} ((F f) = (F g)))
\mvdash{} \mexists{}B:\mBbbN{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}. (|F f| \mleq{} B)
By
Latex:
Assert \mkleeneopen{}\mexists{}B:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} \mBbbB{}. (|F (\mlambda{}i.if i <z n then s i else ff fi )| \mleq{} B)\mkleeneclose{}\mcdot{}
Home
Index