Nuprl Definition : name-morph-domain
name-morph-domain(f;I) == nameset(filter(λx.isname(f x);I))
Definitions occuring in Statement :
isname: isname(z),
nameset: nameset(L),
filter: filter(P;l),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
nameset: nameset(L),
filter: filter(P;l),
lambda: λx.A[x],
isname: isname(z),
apply: f a
FDL editor aliases :
name-morph-domain
Latex:
name-morph-domain(f;I) == nameset(filter(\mlambda{}x.isname(f x);I))
Date html generated:
2016_05_20-AM-09_30_22
Last ObjectModification:
2015_09_23-AM-09_29_30
Theory : cubical!sets
Home
Index