Nuprl Definition : no-classrel-in-interval
(no X between start and e) == ∀e'<e.start ≤loc e' ⇒ (∀w:A. (¬w ∈ X(e')))
Definitions occuring in Statement :
classrel: v ∈ X(e),
eo-forward: eo.e,
alle-lt: ∀e<e'.P[e],
es-le: e ≤loc e' ,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q
FDL editor aliases :
no-classrel-in-interval
(no X between start and e) == \mforall{}e'<e.start \mleq{}loc e' {}\mRightarrow{} (\mforall{}w:A. (\mneg{}w \mmember{} X(e')))
Date html generated:
2015_07_17-PM-00_29_34
Last ObjectModification:
2012_02_25-PM-01_16_21
Home
Index