---

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

∀[x:ℕ∞]. (¬ni-eventually-equal(x;0∞) ⇐⇒ x = ∞ ∈ ℕ∞)
BY
{ Auto }

1
1. x : ℕ∞
2. ¬ni-eventually-equal(x;0∞)
⊢ x = ∞ ∈ ℕ∞

2
1. x : ℕ∞
2. x = ∞ ∈ ℕ∞
⊢ ¬ni-eventually-equal(x;0∞)

---

Latex:

---

Latex:
\mforall{}[x:\mBbbN{}\minfty{}].  (\mneg{}ni-eventually-equal(x;0\minfty{})  \mLeftarrow{}{}\mRightarrow{}  x  =  \minfty{})


By

---

Latex:
Auto

---

Home Index