---

Step * of Lemma rnonneg_functionality

∀x,y:ℝ.  rnonneg(x) ⇐⇒ rnonneg(y) supposing x = y
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "rnonneg-iff" 0 THENA Auto)
   THEN (Assert bdd-diff(x;y) BY
               (Unfold `req` -1 THEN With ⌜4⌝ (D 0)⋅ THEN Auto))
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    rnonneg(x)  \mLeftarrow{}{}\mRightarrow{}  rnonneg(y)  supposing  x  =  y


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "rnonneg-iff"  0  THENA  Auto)
  THEN  (Assert  bdd-diff(x;y)  BY
                          (Unfold  `req`  -1  THEN  With  \mkleeneopen{}4\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index