Nuprl Definition : Q-R-pre-preserving
f is Q-R-pre-preserving on P == ∀e,e':{e:E| P e} . ((Q (f e) (f e')) ⇒ (R e e'))
Definitions occuring in Statement :
es-E: E,
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a
FDL editor aliases :
Q-R-pre-preserving
Q-R-pre-preserving
f is Q-R-pre-preserving on P == \mforall{}e,e':\{e:E| P e\} . ((Q (f e) (f e')) {}\mRightarrow{} (R e e'))
Date html generated:
2015_07_17-AM-09_02_53
Last ObjectModification:
2013_03_25-PM-01_55_57
Home
Index