Nuprl Definition : no-prior-classrel
(no X prior to e) == 
e'<e.w:A. (
w 
X(e'))
Proof not projected
Definitions occuring in Statement :
classrel: v X(e),
alle-lt: e<e'.P[e],
all: x:A. B[x],
not: A
FDL editor aliases :
no-prior-classrel
(no X prior to e) == \mforall{}e'<e.\mforall{}w:A. (\mneg{}w \mmember{} X(e'))
Date html generated:
2011_10_20-PM-03_19_03
Last ObjectModification:
2011_08_15-PM-04_58_12
Home
Index