---

Step * of Lemma iproper-length

∀I:Interval. ((i-finite(I) ∧ iproper(I)) ⇒ (r0 < |I|))
BY
{ (Auto THEN (D -1 THENA Auto) THEN Unfold `i-length` 0 THEN nRAdd ⌜left-endpoint(I)⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I:Interval.  ((i-finite(I)  \mwedge{}  iproper(I))  {}\mRightarrow{}  (r0  <  |I|))


By

---

Latex:
(Auto  THEN  (D  -1  THENA  Auto)  THEN  Unfold  `i-length`  0  THEN  nRAdd  \mkleeneopen{}left-endpoint(I)\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index