Nuprl Definition : existse-between3
∃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-between3
existse-between3
\mexists{}e\mmember{}(e1,e2].P[e] == \mexists{}e:E. (((e1 <loc e) \mwedge{} e \mleq{}loc e2 ) c\mwedge{} P[e])
Date html generated:
2015_07_17-AM-08_48_11
Last ObjectModification:
2013_03_25-PM-01_50_07
Home
Index