Nuprl Definition : existse-between1
∃e∈[e1,e2).P[e] == ∃e:E. ((e1 ≤loc e ∧ (e <loc e2)) c∧ P[e])
Definitions occuring in Statement :
es-le: e ≤loc e' ,
es-locl: (e <loc e'),
es-E: E,
cand: A c∧ B,
exists: ∃x:A. B[x],
and: P ∧ Q
FDL editor aliases :
existse-between1
existse-between1
Latex:
\mexists{}e\mmember{}[e1,e2).P[e] == \mexists{}e:E. ((e1 \mleq{}loc e \mwedge{} (e <loc e2)) c\mwedge{} P[e])
Date html generated:
2016_05_16-AM-09_43_47
Last ObjectModification:
2013_03_25-PM-01_49_48
Theory : new!event-ordering
Home
Index