Step
*
of Lemma
reals-uncountable-simple
∀f:ℕ ⟶ ℝ. (¬Surj(ℕ;ℝ;f))
BY
{ (Auto THEN D 0 THEN Auto THEN ((InstLemma Obid: reals-uncountable) [⌜f⌝;⌜r0⌝;⌜r1⌝]⋅ THEN Auto) THEN ExRepD) }
1
1. f : ℕ ⟶ ℝ@i
2. Surj(ℕ;ℝ;f)@i
3. u : ℝ
4. r0 ≤ u
5. u ≤ r1
6. ∀n:ℕ. u ≠ f n
⊢ False
Latex:
Latex:
\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbR{}. (\mneg{}Surj(\mBbbN{};\mBbbR{};f))
By
Latex:
(Auto
THEN D 0
THEN Auto
THEN ((InstLemma Obid: reals-uncountable) [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}r1\mkleeneclose{}]\mcdot{} THEN Auto)
THEN ExRepD)
Home
Index