Nuprl Definition : no-classrel-in-interval

(no X between start and e) ==  ∀e'<e.start ≤loc e'  ⇒ (∀w:A. (¬w ∈ X(e')))


Definitions occuring in Statement :  classrel: v ∈ X(e),  eo-forward: eo.e,  alle-lt: ∀e<e'.P[e],  es-le: e ≤loc e' ,  all: ∀x:A. B[x],  not: ¬A,  implies: P ⇒ Q
FDL editor aliases :  no-classrel-in-interval
Latex:
(no  X  between  start  and  e)  ==    \mforall{}e'<e.start  \mleq{}loc  e'    {}\mRightarrow{}  (\mforall{}w:A.  (\mneg{}w  \mmember{}  X(e')))


Date html generated: 2016_05_16-PM-02_00_33
Last ObjectModification: 2012_02_25-PM-01_16_21

Theory : event-ordering


Home Index