---

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


1. a : ℕ∞
⊢ ∃n:ℕ. ∀m:{n...}. a m = a m
BY
{ (With ⌜0⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}\minfty{}
\mvdash{}  \mexists{}n:\mBbbN{}.  \mforall{}m:\{n...\}.  a  m  =  a  m


By

---

Latex:
(With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index