Nuprl Definition : es-weak-joint-embedding
es-weak-joint-embedding(Info;eo1;eo2;eo;f;g) ==
(f embeds eo1 into eo)
∧ es-local-embedding(Info;eo2;eo;g)
∧ (∀e:E. ((∃e1:E. (e = (f e1) ∈ E)) ∨ (∃e2:E. (e = (g e2) ∈ E))))
∧ (∀x,y:E. ((x < y) ⇒ ((g x < g y) ∨ (∃z:E. ((g y) = (f z) ∈ E)))))
Definitions occuring in Statement :
es-embedding: (f embeds eo1 into eo2),
es-local-embedding: es-local-embedding(Info;eo1;eo2;f),
es-causl: (e < e'),
es-E: E,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T
FDL editor aliases :
es-weak-joint-embedding
es-weak-joint-embedding(Info;eo1;eo2;eo;f;g) ==
(f embeds eo1 into eo)
\mwedge{} es-local-embedding(Info;eo2;eo;g)
\mwedge{} (\mforall{}e:E. ((\mexists{}e1:E. (e = (f e1))) \mvee{} (\mexists{}e2:E. (e = (g e2)))))
\mwedge{} (\mforall{}x,y:E. ((x < y) {}\mRightarrow{} ((g x < g y) \mvee{} (\mexists{}z:E. ((g y) = (f z))))))
Date html generated:
2015_07_17-PM-00_12_37
Last ObjectModification:
2014_08_11-PM-00_09_21
Home
Index