Nuprl Lemma : es-subinterval

es:EO. ∀e2,e1:E.  (e1 ≤loc e2   (∀n:ℕ(∃e∈(e1,e2].||[e1, pred(e)]|| n ∈ ℤsupposing (n < ||[e1, e2]|| and 0 < n))\000C)


Definitions occuring in Statement :  existse-between3: e∈(e1,e2].P[e] es-interval: [e, e'] es-le: e ≤loc e'  es-pred: pred(e) es-E: E event_ordering: EO length: ||as|| nat: less_than: a < b uimplies: supposing a all: x:A. B[x] implies:  Q natural_number: $n int: equal: t ∈ T
Lemmas :  member-less_than length_wf es-E_wf es-interval_wf es-le-iff less_than_wf nat_wf es-le_wf es-pred_wf es-pred-locl decidable__lt es-locl_transitivity1 es-le_weakening es-locl-first assert_elim btrue_neq_bfalse assert_wf es-first_wf2 es-le-pred length-append length_of_cons_lemma length_of_nil_lemma squash_wf true_wf list_wf es-interval-less iff_weakening_equal es-le-self decidable__equal_int false_wf not-equal-2 less-iff-le condition-implies-le add-associates minus-add minus-one-mul add-swap add-commutes zero-add add_functionality_wrt_le le-add-cancel2 le-add-cancel es-locl_wf es-interval-eq add-zero
\mforall{}es:EO.  \mforall{}e2,e1:E.
    (e1  \mleq{}loc  e2    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (\mexists{}e\mmember{}(e1,e2].||[e1,  pred(e)]||  =  n)  supposing  (n  <  ||[e1,  e2]||  and  0  <  n)))

Date html generated: 2015_07_17-AM-08_48_40
Last ObjectModification: 2015_02_04-PM-05_55_57

Home Index