Nuprl Definition : setunionfun
⋃x∈s.f[x] == let T,g = s in <t:T × set-dom(f[g t]), λp.let t,d = p in set-item(f[g t];d)>
Definitions occuring in Statement :
set-item: set-item(s;x),
set-dom: set-dom(s),
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
product: x:A × B[x]
Definitions occuring in definition :
apply: f a,
set-item: set-item(s;x),
spread: spread def,
lambda: λx.A[x],
set-dom: set-dom(s),
product: x:A × B[x],
pair: <a, b>
FDL editor aliases :
setunionfun
Latex:
\mcup{}x\mmember{}s.f[x] == let T,g = s in <t:T \mtimes{} set-dom(f[g t]), \mlambda{}p.let t,d = p in set-item(f[g t];d)>
Date html generated:
2018_07_29-AM-09_52_44
Last ObjectModification:
2018_07_18-PM-02_29_45
Theory : constructive!set!theory
Home
Index