---

Step * 1 1 of Lemma reals-uncountable-simple


1. f : ℕ ⟶ ℝ@i
2. u : ℝ
3. r0 ≤ u
4. u ≤ r1
5. ∀n:ℕ. u ≠ f n
6. a : ℕ@i
7. (f a) = u ∈ ℝ@i
8. u ≠ u
⊢ False
BY
{ (FLemma `rneq_irreflexivity` [-1] THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}@i
2.  u  :  \mBbbR{}
3.  r0  \mleq{}  u
4.  u  \mleq{}  r1
5.  \mforall{}n:\mBbbN{}.  u  \mneq{}  f  n
6.  a  :  \mBbbN{}@i
7.  (f  a)  =  u@i
8.  u  \mneq{}  u
\mvdash{}  False


By

---

Latex:
(FLemma  `rneq\_irreflexivity`  [-1]  THEN  Auto)\mcdot{}

---

Home Index