Nuprl Definition : sigmaset
Σa:A.B[a] ==  let T,f = A in <t:T × set-dom(B[f t]), λp.let t,s = p in (f t,set-item(B[f t];s))>
Definitions occuring in Statement : 
orderedpairset: (a,b)
, 
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)
, 
orderedpairset: (a,b)
, 
spread: spread def, 
lambda: λx.A[x]
, 
set-dom: set-dom(s)
, 
product: x:A × B[x]
, 
pair: <a, b>
FDL editor aliases : 
sigmaset
Latex:
\mSigma{}a:A.B[a]  ==    let  T,f  =  A  in  <t:T  \mtimes{}  set-dom(B[f  t]),  \mlambda{}p.let  t,s  =  p  in  (f  t,set-item(B[f  t];s))>
Date html generated:
2018_07_29-AM-10_04_06
Last ObjectModification:
2018_07_18-PM-03_43_50
Theory : constructive!set!theory
Home
Index