Nuprl Definition : es-embedding
(f embeds eo1 into eo2) == es-local-embedding(Info;eo1;eo2;f) ∧ (∀e,e':E. ((e' < e) ⇒ (f e' < f e)))
Definitions occuring in Statement :
es-local-embedding: es-local-embedding(Info;eo1;eo2;f),
es-causl: (e < e'),
es-E: E,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a
FDL editor aliases :
es-embedding
(f embeds eo1 into eo2) == es-local-embedding(Info;eo1;eo2;f) \mwedge{} (\mforall{}e,e':E. ((e' < e) {}\mRightarrow{} (f e' < f e\000C)))
Date html generated:
2015_07_17-PM-00_11_40
Last ObjectModification:
2014_08_11-AM-11_45_18
Home
Index