---

Step * 2 1 of Lemma not-ni-eventually-equal-inf


1. x : ℕ∞
2. x = ∞ ∈ ℕ∞
3. n : ℕ
4. ∀m:{n...}. ∞ m = 0∞ m
5. ∞ n = 0∞ n
⊢ False
BY
{ RepUR ``nat2inf nat-inf-infinity`` -1 }

1
1. x : ℕ∞
2. x = ∞ ∈ ℕ∞
3. n : ℕ
4. ∀m:{n...}. ∞ m = 0∞ m
5. tt = n <z 0
⊢ False

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\minfty{}
2.  x  =  \minfty{}
3.  n  :  \mBbbN{}
4.  \mforall{}m:\{n...\}.  \minfty{}  m  =  0\minfty{}  m
5.  \minfty{}  n  =  0\minfty{}  n
\mvdash{}  False


By

---

Latex:
RepUR  ``nat2inf  nat-inf-infinity``  -1

---

Home Index