Step * of Lemma icompact-length-nonneg

[I:Interval]. r0 ≤ |I| supposing icompact(I)
BY
(Auto THEN -1 THEN Auto THEN Unfold `i-length` THEN nRAdd ⌜left-endpoint(I)⌝ 0⋅}

1
1. 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