Nuprl Definition : es-local-embedding
es-local-embedding(Info;eo1;eo2;f) ==
∀e:E. ((loc(e) = loc(f e) ∈ Id) ∧ (map(λx.info(x);≤loc(e)) = map(λx.info(x);≤loc(f e)) ∈ (Info List)))
Definitions occuring in Statement :
es-info: info(e),
es-le-before: ≤loc(e),
es-loc: loc(e),
es-E: E,
Id: Id,
map: map(f;as),
list: T List,
all: ∀x:A. B[x],
and: P ∧ Q,
apply: f a,
lambda: λx.A[x],
equal: s = t ∈ T
FDL editor aliases :
es-local-embedding
es-local-embedding(Info;eo1;eo2;f) ==
\mforall{}e:E. ((loc(e) = loc(f e)) \mwedge{} (map(\mlambda{}x.info(x);\mleq{}loc(e)) = map(\mlambda{}x.info(x);\mleq{}loc(f e))))
Date html generated:
2015_07_17-PM-00_11_20
Last ObjectModification:
2014_08_11-AM-11_43_44
Home
Index