Step
*
of Lemma
icompact-length-nonneg
∀[I:Interval]. r0 ≤ |I| supposing icompact(I)
BY
{ (Auto THEN D -1 THEN Auto THEN Unfold `i-length` 0 THEN nRAdd ⌜left-endpoint(I)⌝ 0⋅) }
1
1. I : Interval
2. i-nonvoid(I)
3. i-closed(I)
4. i-finite(I)
⊢ left-endpoint(I) ≤ right-endpoint(I)
Latex:
Latex:
\mforall{}[I:Interval].  r0  \mleq{}  |I|  supposing  icompact(I)
By
Latex:
(Auto  THEN  D  -1  THEN  Auto  THEN  Unfold  `i-length`  0  THEN  nRAdd  \mkleeneopen{}left-endpoint(I)\mkleeneclose{}  0\mcdot{})
Home
Index