---

Step * of Lemma std-is-infinitesmal

is-infinitesmal(∈)
BY
{ ((D 0 THEN Auto) THEN D 0 With ⌜n⌝  THEN Auto THEN RepUR ``std-infinitesmal rstar rabs* rfun*`` 0) }

1
1. n : ℕ+
2. m : {n...}
⊢ |(r1/r(m + 1))| < (r1/r(n))

---

Latex:

---

Latex:
is-infinitesmal(\mmember{})


By

---

Latex:
((D  0  THEN  Auto)  THEN  D  0  With  \mkleeneopen{}n\mkleeneclose{}    THEN  Auto  THEN  RepUR  ``std-infinitesmal  rstar  rabs*  rfun*``  0)

---

Home Index