Nuprl Definition : regext
By forming a set indexed by a suitable W type, we get a Regular set r for which
(a ⊆ r) provided that set a is transitive.
See subset-regext and regext-Regularset.⋅
regext(a) == let T,f = a in λw.regextfun(f;w)"(W(T;x.set-dom(f x)))
Definitions occuring in Statement :
regextfun: regextfun(f;w),
mk-set: f"(T),
set-dom: set-dom(s),
W: W(A;a.B[a]),
apply: f a,
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
spread: spread def,
mk-set: f"(T),
W: W(A;a.B[a]),
set-dom: set-dom(s),
apply: f a,
lambda: λx.A[x],
regextfun: Error :regextfun
FDL editor aliases :
regext
Latex:
regext(a) == let T,f = a in \mlambda{}w.regextfun(f;w)"(W(T;x.set-dom(f x)))
Date html generated:
2018_07_29-AM-10_07_11
Last ObjectModification:
2018_05_30-PM-07_05_57
Theory : constructive!set!theory
Home
Index