---

Step * of Lemma rpositive_functionality

∀x,y:ℝ.  rpositive(x) ⇐⇒ rpositive(y) supposing x = y
BY
{ (Assert ⌜∀x,y:ℝ.  rpositive(x) ⇒ rpositive(y) supposing x = y⌝⋅
   THEN Auto
   THEN Try ((InstHyp [⌜y⌝;⌜x⌝] 1⋅ THEN Auto))
   THEN (RWO "rpositive-iff" (-1) THENA Auto)
   THEN (RWO "rpositive-iff" 0 THENA Auto)
   THEN (Assert bdd-diff(x;y) BY
               (With ⌜4⌝ (D 0)⋅ THEN Auto))
   THEN RWO "-1<" 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}x,y:\mBbbR{}.    rpositive(x)  {}\mRightarrow{}  rpositive(y)  supposing  x  =  y\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Try  ((InstHyp  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  1\mcdot{}  THEN  Auto))
  THEN  (RWO  "rpositive-iff"  (-1)  THENA  Auto)
  THEN  (RWO  "rpositive-iff"  0  THENA  Auto)
  THEN  (Assert  bdd-diff(x;y)  BY
                          (With  \mkleeneopen{}4\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
  THEN  RWO  "-1<"  0
  THEN  Auto)

---

Home Index