---

Step * 2 of Lemma ni-eventually-equal-equiv


1. ∀a:ℕ∞. ∃n:ℕ. ∀m:{n...}. a m = a m
2. a : ℕ∞
3. b : ℕ∞
4. ∃n:ℕ. ∀m:{n...}. a m = b m
⊢ ∃n:ℕ. ∀m:{n...}. b m = a m
BY
{ (ParallelLast THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}a:\mBbbN{}\minfty{}.  \mexists{}n:\mBbbN{}.  \mforall{}m:\{n...\}.  a  m  =  a  m
2.  a  :  \mBbbN{}\minfty{}
3.  b  :  \mBbbN{}\minfty{}
4.  \mexists{}n:\mBbbN{}.  \mforall{}m:\{n...\}.  a  m  =  b  m
\mvdash{}  \mexists{}n:\mBbbN{}.  \mforall{}m:\{n...\}.  b  m  =  a  m


By

---

Latex:
(ParallelLast  THEN  Auto)

---

Home Index