Nuprl Definition : piset
piset(A;a.B[a]) == let T,f = A in <t:T ⟶ set-dom(B[f t]), λg.<T, λt.(f t,set-item(B[f t];g t))>>
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],
function: x:A ⟶ B[x],
spread: spread def,
pair: <a, b>
Definitions occuring in definition :
apply: f a,
set-item: set-item(s;x),
orderedpairset: (a,b),
lambda: λx.A[x],
pair: <a, b>,
set-dom: set-dom(s),
function: x:A ⟶ B[x],
spread: spread def
FDL editor aliases :
piset
Latex:
piset(A;a.B[a]) == let T,f = A in <t:T {}\mrightarrow{} set-dom(B[f t]), \mlambda{}g.<T, \mlambda{}t.(f t,set-item(B[f t];g t))>>
Date html generated:
2018_07_29-AM-10_04_19
Last ObjectModification:
2018_07_18-PM-03_26_10
Theory : constructive!set!theory
Home
Index