Nuprl Definition : no-prior-classrel
(no X prior to e) == ∀e'<e.∀w:A. (¬w ∈ X(e'))
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:
2015_07_17-PM-00_29_14
Last ObjectModification:
2012_02_25-PM-01_16_09
Home
Index