---

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


1. x : ℕ ⟶ 𝔹
2. ∀n:ℕ. ((↑(x (n + 1))) ⇒ (↑(x n)))
3. ¬ni-eventually-equal(x;0∞)
4. i : ℕ
⊢ x i = ∞ i
BY
{ (RepUR ``nat-inf-infinity`` 0 THEN AutoBoolCase ⌜x i⌝⋅ THEN D -3) }

1
1. x : ℕ ⟶ 𝔹
2. ∀n:ℕ. ((↑(x (n + 1))) ⇒ (↑(x n)))
3. i : ℕ
4. ¬↑(x i)
⊢ ni-eventually-equal(x;0∞)

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
2.  \mforall{}n:\mBbbN{}.  ((\muparrow{}(x  (n  +  1)))  {}\mRightarrow{}  (\muparrow{}(x  n)))
3.  \mneg{}ni-eventually-equal(x;0\minfty{})
4.  i  :  \mBbbN{}
\mvdash{}  x  i  =  \minfty{}  i


By

---

Latex:
(RepUR  ``nat-inf-infinity``  0  THEN  AutoBoolCase  \mkleeneopen{}x  i\mkleeneclose{}\mcdot{}  THEN  D  -3)

---

Home Index