---

Step * of Lemma icompact-endpoints-rleq

∀[I:Interval]. left-endpoint(I) ≤ right-endpoint(I) supposing icompact(I)
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN ((FLemma `icompact-length-nonneg` [-1]) THENA Auto)
   THEN RepUR ``i-length`` -1
   THEN (nRAdd ⌜left-endpoint(I)⌝ (-1))⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[I:Interval].  left-endpoint(I)  \mleq{}  right-endpoint(I)  supposing  icompact(I)


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  ((FLemma  `icompact-length-nonneg`  [-1])  THENA  Auto)
  THEN  RepUR  ``i-length``  -1
  THEN  (nRAdd  \mkleeneopen{}left-endpoint(I)\mkleeneclose{}  (-1))\mcdot{}
  THEN  Auto)

---

Home Index