Nuprl Lemma : es-open-interval-ordered-inst
∀es:EO. ∀e1,e2:E. ∀n1,n2:ℕ||(e1, e2)||.  (n1 < n2 
⇒ ((e1, e2)[n1] <loc (e1, e2)[n2]))
Proof
Definitions occuring in Statement : 
es-open-interval: (e, e')
, 
es-locl: (e <loc e')
, 
es-E: E
, 
event_ordering: EO
, 
select: L[n]
, 
length: ||as||
, 
int_seg: {i..j-}
, 
less_than: a < b
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
natural_number: $n
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
member: t ∈ T
, 
l-ordered: l-ordered(T;x,y.R[x; y];L)
, 
uall: ∀[x:A]. B[x]
, 
uimplies: b supposing a
, 
prop: ℙ
, 
int_seg: {i..j-}
Latex:
\mforall{}es:EO.  \mforall{}e1,e2:E.  \mforall{}n1,n2:\mBbbN{}||(e1,  e2)||.    (n1  <  n2  {}\mRightarrow{}  ((e1,  e2)[n1]  <loc  (e1,  e2)[n2]))
Date html generated:
2016_05_16-AM-09_36_16
Last ObjectModification:
2015_12_28-PM-09_45_18
Theory : new!event-ordering
Home
Index