---

Step * of Lemma es-interval-non-zero

∀es:EO. ∀e,e':E.  (e ≤loc e'  ⇐⇒ 0 < ||[e, e']||)
BY
{ Auto }

1
1. es : EO@i'
2. e : E@i
3. e' : E@i
4. e ≤loc e' @i
⊢ 0 < ||[e, e']||

2
1. es : EO@i'
2. e : E@i
3. e' : E@i
4. 0 < ||[e, e']||@i
⊢ e ≤loc e' 

---

Latex:


\mforall{}es:EO.  \mforall{}e,e':E.    (e  \mleq{}loc  e'    \mLeftarrow{}{}\mRightarrow{}  0  <  ||[e,  e']||)


By

Auto

---

Home Index