---

Step * of Lemma inf-as-sup

∀[A:Set(ℝ)]. ∀b:ℝ. (inf(A) = b ⇐⇒ sup(-(A)) = -(b))
BY
{ (RepUR ``inf sup lower-bound upper-bound`` 0
   THEN Auto
   THEN Reduce 0
   THEN Try ((nRMul ⌜r(-1)⌝ 0⋅ THEN Auto THEN BackThruSomeHyp))
   THEN Try ((RWO "rminus-rminus-eq" 0 THEN Auto))
   THEN ∀h:hyp. (((InstHyp [⌜e⌝] h)⋅ THENA Complete (Auto))
                 THEN D -1
                 THEN ((InstConcl [⌜-(x)⌝])⋅ THENA Auto)
                 THEN ParallelLast
                 THEN Try ((RWO "rminus-rminus-eq" 0 THEN Auto))
                 THEN nRMul ⌜r(-1)⌝ 0⋅
                 THEN Auto
                 THEN (nRNorm (-1))
                 THEN Auto) ) }

---

Latex:

---

Latex:
\mforall{}[A:Set(\mBbbR{})].  \mforall{}b:\mBbbR{}.  (inf(A)  =  b  \mLeftarrow{}{}\mRightarrow{}  sup(-(A))  =  -(b))


By

---

Latex:
(RepUR  ``inf  sup  lower-bound  upper-bound``  0
  THEN  Auto
  THEN  Reduce  0
  THEN  Try  ((nRMul  \mkleeneopen{}r(-1)\mkleeneclose{}  0\mcdot{}  THEN  Auto  THEN  BackThruSomeHyp))
  THEN  Try  ((RWO  "rminus-rminus-eq"  0  THEN  Auto))
  THEN  \mforall{}h:hyp.  (((InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  h)\mcdot{}  THENA  Complete  (Auto))
                              THEN  D  -1
                              THEN  ((InstConcl  [\mkleeneopen{}-(x)\mkleeneclose{}])\mcdot{}  THENA  Auto)
                              THEN  ParallelLast
                              THEN  Try  ((RWO  "rminus-rminus-eq"  0  THEN  Auto))
                              THEN  nRMul  \mkleeneopen{}r(-1)\mkleeneclose{}  0\mcdot{}
                              THEN  Auto
                              THEN  (nRNorm  (-1))
                              THEN  Auto)  )

---

Home Index