---

Step * of Lemma infinitesmal-difference

∀[x,y:ℝ].  uiff(x = y;∀[k:ℕ+]. (|x - y| ≤ (r1/r(k))))
BY
{ ((UnivCD THENA (Auto THEN BLemma `rneq-int` THEN Auto))
   THEN (RWO "infinitesmal-zero<" 0 THENA (Auto THEN BLemma `rneq-int` THEN Auto))
   ) }

1
1. x : ℝ
2. y : ℝ
⊢ uiff(x = y;(x - y) = r0)

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    uiff(x  =  y;\mforall{}[k:\mBbbN{}\msupplus{}].  (|x  -  y|  \mleq{}  (r1/r(k))))


By

---

Latex:
((UnivCD  THENA  (Auto  THEN  BLemma  `rneq-int`  THEN  Auto))
  THEN  (RWO  "infinitesmal-zero<"  0  THENA  (Auto  THEN  BLemma  `rneq-int`  THEN  Auto))
  )

---

Home Index