Nuprl Definition : no-classrel-in-interval

(no X between start and e) ==

e'<e.start

loc e'

(

w:A. (

w

X(e')))

Proof not projected

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: 2011_10_20-PM-03_19_18 Last ObjectModification: 2011_09_05-PM-06_29_22 Home Index