Step * 2 1 1 of Lemma countable-Heine-Borel-proper


1. : ℝ
2. {b:ℝa < b} 
3. [C] : ℕ ⟶ {x:ℝx ∈ [a, b]}  ⟶ ℙ
4. ∀n:ℕ. ∀x:{x:ℝx ∈ [a, b]} . ∀y:{y:{x:ℝx ∈ [a, b]} y} .  (C[n;x]  C[n;y])
5. ∀x:{x:ℝx ∈ [a, b]} . ∃n:ℕC[n;x]
6. ∀f:ℕ ⟶ 𝔹. ∃n:ℕC[n;cantor-to-interval(a;b;f)]
7. : ℕ
8. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. C[n;cantor-to-interval(a;b;f)]
9. {x:ℝx ∈ [a, b]} 
10. : ℕ ⟶ 𝔹
11. cantor-to-interval(a;b;f) x
12. : ℕk
13. C[n;cantor-to-interval(a;b;f)]
⊢ C[n;x]
BY
(InstHyp [⌜n⌝;⌜cantor-to-interval(a;b;f)⌝;⌜x⌝4⋅ THEN Auto) }


Latex:


Latex:

1.  a  :  \mBbbR{}
2.  b  :  \{b:\mBbbR{}|  a  <  b\} 
3.  [C]  :  \mBbbN{}  {}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}    {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}n:\mBbbN{}.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  |  x  =  y\}  .    (C[n;x]  {}\mRightarrow{}  C[n;y])
5.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  \mexists{}n:\mBbbN{}.  C[n;x]
6.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}.  C[n;cantor-to-interval(a;b;f)]
7.  k  :  \mBbbN{}
8.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}k.  C[n;cantor-to-interval(a;b;f)]
9.  x  :  \{x:\mBbbR{}|  x  \mmember{}  [a,  b]\} 
10.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
11.  cantor-to-interval(a;b;f)  =  x
12.  n  :  \mBbbN{}k
13.  C[n;cantor-to-interval(a;b;f)]
\mvdash{}  C[n;x]


By


Latex:
(InstHyp  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}cantor-to-interval(a;b;f)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  4\mcdot{}  THEN  Auto)




Home Index