Step
*
1
2
of Lemma
cantor-to-int-bounded
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)
BY
{ (RepeatFor 2 (ParallelLast) THEN NthHypEq (-1) THEN RepeatFor 2 (EqCDA) THEN BHyp 3 THEN Auto) }
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)))
4. \mexists{}B:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} \mBbbB{}. (|F (\mlambda{}i.if i <z n then s i else ff fi )| \mleq{} B)
\mvdash{} \mexists{}B:\mBbbN{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}. (|F f| \mleq{} B)
By
Latex:
(RepeatFor 2 (ParallelLast) THEN NthHypEq (-1) THEN RepeatFor 2 (EqCDA) THEN BHyp 3 THEN Auto)
Home
Index