---

Step * of Lemma icompact-endpoints

∀I:Interval. (icompact(I) ⇒ ((left-endpoint(I) ∈ I) ∧ (right-endpoint(I) ∈ I)))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN ((FLemma `icompact-length-nonneg` [-1]) THENA Auto)
   THEN (MoveToConcl (-1))
   THEN RepeatFor 2 (D -1)
   THEN D 1
   THEN D 1
   THEN RepUR ``i-finite`` -1
   THEN D -1
   THEN Try (Trivial)
   THEN D 2
   THEN All Reduce
   THEN Try (Trivial)
   THEN D 1
   THEN D 2
   THEN Try (Complete (∀h:hyp. (RepUR ``i-closed`` h THEN D h THEN SplitOrHyps THEN Auto) ))
   THEN RepUR ``i-length left-endpoint right-endpoint endpoints i-member`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I:Interval.  (icompact(I)  {}\mRightarrow{}  ((left-endpoint(I)  \mmember{}  I)  \mwedge{}  (right-endpoint(I)  \mmember{}  I)))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  ((FLemma  `icompact-length-nonneg`  [-1])  THENA  Auto)
  THEN  (MoveToConcl  (-1))
  THEN  RepeatFor  2  (D  -1)
  THEN  D  1
  THEN  D  1
  THEN  RepUR  ``i-finite``  -1
  THEN  D  -1
  THEN  Try  (Trivial)
  THEN  D  2
  THEN  All  Reduce
  THEN  Try  (Trivial)
  THEN  D  1
  THEN  D  2
  THEN  Try  (Complete  (\mforall{}h:hyp.  (RepUR  ``i-closed``  h  THEN  D  h  THEN  SplitOrHyps  THEN  Auto)  ))
  THEN  RepUR  ``i-length  left-endpoint  right-endpoint  endpoints  i-member``  0
  THEN  Auto)

---

Home Index