Nuprl Definition : existse-at
∃e@i.P[e] == ∃e:E. ((loc(e) = i ∈ Id) ∧ P[e])
Definitions occuring in Statement :
es-loc: loc(e),
es-E: E,
Id: Id,
exists: ∃x:A. B[x],
and: P ∧ Q,
equal: s = t ∈ T
FDL editor aliases :
existse-at
existse-at
\mexists{}e@i.P[e] == \mexists{}e:E. ((loc(e) = i) \mwedge{} P[e])
Date html generated:
2015_07_17-AM-08_45_34
Last ObjectModification:
2013_03_25-PM-01_49_18
Home
Index