---

Step * of Lemma proper-interval-to-int-bounded

∀a,b:ℝ.
  ∀f:{x:ℝ| x ∈ [a, b]}  ⟶ ℤ. ∃B:ℕ. ∀x:{x:ℝ| x ∈ [a, b]} . ∃y:{x:ℝ| x ∈ [a, b]} . ((x = y) ∧ (|f y| ≤ B)) supposing a < \000Cb
BY
{ (InstLemma `cantor-to-interval-onto-proper` []⋅
   THEN RepeatFor 3 (ParallelLast')
   THEN (Assert ∀x:{x:ℝ| x ∈ [a, b]} . ∃p:ℕ ⟶ 𝔹. (cantor-to-interval(a;b;p) = x) BY
               (ParallelLast THEN BHyp -1 THEN Auto))
   THEN (D 0 THENA Auto)
   THEN (InstLemma `cantor-to-int-bounded` [⌜λp.(f cantor-to-interval(a;b;p))⌝]⋅ THENA Auto)
   THEN ParallelLast
   THEN ParallelOp 5
   THEN D -1
   THEN (D -4 With ⌜p⌝  THENA Auto)
   THEN Reduce -1) }

1
1. a : ℝ
2. b : ℝ
3. [%] : a < b
4. ∀x:ℝ. ((a ≤ x) ⇒ (x ≤ b) ⇒ (∃f:ℕ ⟶ 𝔹. (cantor-to-interval(a;b;f) = x)))
5. ∀x:{x:ℝ| x ∈ [a, b]} . ∃p:ℕ ⟶ 𝔹. (cantor-to-interval(a;b;p) = x)
6. f : {x:ℝ| x ∈ [a, b]}  ⟶ ℤ
7. B : ℕ
8. x : {x:ℝ| x ∈ [a, b]} 
9. p : ℕ ⟶ 𝔹
10. cantor-to-interval(a;b;p) = x
11. |f cantor-to-interval(a;b;p)| ≤ B
⊢ ∃y:{x:ℝ| x ∈ [a, b]} . ((x = y) ∧ (|f y| ≤ B))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.
    \mforall{}f:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}    {}\mrightarrow{}  \mBbbZ{}
        \mexists{}B:\mBbbN{}.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  \mexists{}y:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  ((x  =  y)  \mwedge{}  (|f  y|  \mleq{}  B)) 
    supposing  a  <  b


By

---

Latex:
(InstLemma  `cantor-to-interval-onto-proper`  []\mcdot{}
  THEN  RepeatFor  3  (ParallelLast')
  THEN  (Assert  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  \mexists{}p:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (cantor-to-interval(a;b;p)  =  x)  BY
                          (ParallelLast  THEN  BHyp  -1  THEN  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  (InstLemma  `cantor-to-int-bounded`  [\mkleeneopen{}\mlambda{}p.(f  cantor-to-interval(a;b;p))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelLast
  THEN  ParallelOp  5
  THEN  D  -1
  THEN  (D  -4  With  \mkleeneopen{}p\mkleeneclose{}    THENA  Auto)
  THEN  Reduce  -1)

---

Home Index