Nuprl Definition : co-regext
co-regext(a) == let T,f = a in mk-coset(coW(T;x.set-dom(f x));λw.regextfun(f;w))
Definitions occuring in Statement :
regextfun: regextfun(f;w),
set-dom: set-dom(s),
mk-coset: mk-coset(T;f),
coW: coW(A;a.B[a]),
apply: f a,
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
regextfun: regextfun(f;w),
lambda: λx.A[x],
apply: f a,
set-dom: set-dom(s),
coW: coW(A;a.B[a]),
mk-coset: mk-coset(T;f),
spread: spread def
FDL editor aliases :
co-regext
Latex:
co-regext(a) == let T,f = a in mk-coset(coW(T;x.set-dom(f x));\mlambda{}w.regextfun(f;w))
Date html generated:
2018_07_29-AM-10_07_53
Last ObjectModification:
2018_07_21-PM-04_31_53
Theory : constructive!set!theory
Home
Index