---

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