Nuprl Definition : alle-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,
all: ∀x:A. B[x],
implies: P ⇒ Q,
equal: s = t ∈ T
FDL editor aliases :
alle-at
alle-at
\mforall{}e@i.P[e] == \mforall{}e:E. ((loc(e) = i) {}\mRightarrow{} P[e])
Date html generated:
2015_07_17-AM-08_36_01
Last ObjectModification:
2013_03_25-PM-01_45_39
Home
Index