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: 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