---

Step * of Lemma es-open-interval-ordered-inst

∀es:EO. ∀e1,e2:E. ∀n1,n2:ℕ||(e1, e2)||.  (n1 < n2 ⇒ ((e1, e2)[n1] <loc (e1, e2)[n2]))
BY
{ (Auto
   THEN (InstLemma `es-open-interval-ordered` [⌈es⌉;⌈e1⌉;⌈e2⌉]⋅ THENA Auto)
   THEN Unfold `l-ordered` (-1)
   THEN (InstHyp [⌈(e1, e2)[n1]⌉;⌈(e1, e2)[n2]⌉] (-1)⋅ THENM Auto)
   THEN Auto
   THEN BLemma `l_before_select`
   THEN Auto) }

---

Latex:


\mforall{}es:EO.  \mforall{}e1,e2:E.  \mforall{}n1,n2:\mBbbN{}||(e1,  e2)||.    (n1  <  n2  {}\mRightarrow{}  ((e1,  e2)[n1]  <loc  (e1,  e2)[n2]))


By

(Auto
  THEN  (InstLemma  `es-open-interval-ordered`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `l-ordered`  (-1)
  THEN  (InstHyp  [\mkleeneopen{}(e1,  e2)[n1]\mkleeneclose{};\mkleeneopen{}(e1,  e2)[n2]\mkleeneclose{}]  (-1)\mcdot{}  THENM  Auto)
  THEN  Auto
  THEN  BLemma  `l\_before\_select`
  THEN  Auto)

---

Home Index