---

Step * of Lemma totally-bounded-neg

∀[A:Set(ℝ)]. (totally-bounded(A) ⇐⇒ totally-bounded(-(A)))
BY
{ (Auto
   THEN RepeatFor 4 (ParallelLast)
   THEN D -1
   THEN ((InstConcl [⌜λi.-(a i)⌝])⋅ THENA Auto)
   THEN Reduce 0
   THEN ParallelLast
   THEN Try (Complete ((RWO "rminus-rminus-eq" 0 THEN Auto)))
   THEN (Reduce (-1))
   THEN Try (Trivial)
   THEN Auto
   THEN (InstHyp [⌜-(x)⌝] (-3))⋅
   THEN Auto
   THEN Try (Complete ((RWO "rminus-rminus-eq" 0 THEN Auto)))
   THEN ParallelLast
   THEN (RWO "rabs-rminus<" (-1))
   THEN Auto
   THEN (nRNorm (-1))
   THEN Auto
   THEN nRNorm 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Set(\mBbbR{})].  (totally-bounded(A)  \mLeftarrow{}{}\mRightarrow{}  totally-bounded(-(A)))


By

---

Latex:
(Auto
  THEN  RepeatFor  4  (ParallelLast)
  THEN  D  -1
  THEN  ((InstConcl  [\mkleeneopen{}\mlambda{}i.-(a  i)\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  ParallelLast
  THEN  Try  (Complete  ((RWO  "rminus-rminus-eq"  0  THEN  Auto)))
  THEN  (Reduce  (-1))
  THEN  Try  (Trivial)
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}-(x)\mkleeneclose{}]  (-3))\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((RWO  "rminus-rminus-eq"  0  THEN  Auto)))
  THEN  ParallelLast
  THEN  (RWO  "rabs-rminus<"  (-1))
  THEN  Auto
  THEN  (nRNorm  (-1))
  THEN  Auto
  THEN  nRNorm  0
  THEN  Auto)

---

Home Index