Nuprl Lemma : es-p-locl_transitivity2

es:EO. ∀p:E ─→ (E Top). ∀a,b,c:E.  (a p≤  p<  p< c)


Proof




Definitions occuring in Statement :  es-p-le: p≤ e' es-p-locl: p< e' es-E: E event_ordering: EO top: Top all: x:A. B[x] implies:  Q function: x:A ─→ B[x] union: left right
Lemmas :  es-p-locl_wf or_wf equal_wf es-E_wf top_wf event_ordering_wf es-p-locl_transitivity
\mforall{}es:EO.  \mforall{}p:E  {}\mrightarrow{}  (E  +  Top).  \mforall{}a,b,c:E.    (a  p\mleq{}  b  {}\mRightarrow{}  b  p<  c  {}\mRightarrow{}  a  p<  c)



Date html generated: 2015_07_17-AM-09_07_48
Last ObjectModification: 2015_01_27-PM-00_47_30

Home Index