Nuprl Definition : es-joint-embedding
es-joint-embedding(Info;eo1;eo2;eo;f;g) ==
(f embeds eo1 into eo) ∧ (g embeds eo2 into eo) ∧ (∀e:E. ((∃e1:E. (e = (f e1) ∈ E)) ∨ (∃e2:E. (e = (g e2) ∈ E))))
Definitions occuring in Statement :
es-embedding: (f embeds eo1 into eo2),
es-E: E,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
or: P ∨ Q,
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T
FDL editor aliases :
es-joint-embedding
es-joint-embedding(Info;eo1;eo2;eo;f;g) ==
(f embeds eo1 into eo) \mwedge{} (g embeds eo2 into eo) \mwedge{} (\mforall{}e:E. ((\mexists{}e1:E. (e = (f e1))) \mvee{} (\mexists{}e2:E. (e = (g \000Ce2)))))
Date html generated:
2015_07_17-PM-00_12_24
Last ObjectModification:
2014_08_08-PM-09_15_08
Home
Index