Nuprl Definition : fun-graph
fun-graph(b;f) == let T,g = b in <T, λt.(g t,f <g t, mem-mk-set(g;t)>)>
Definitions occuring in Statement :
mem-mk-set: mem-mk-set(f;t),
orderedpairset: (a,b),
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>
Definitions occuring in definition :
mem-mk-set: mem-mk-set(f;t),
apply: f a,
pair: <a, b>,
orderedpairset: (a,b),
lambda: λx.A[x],
spread: spread def
FDL editor aliases :
fun-graph
Latex:
fun-graph(b;f) == let T,g = b in <T, \mlambda{}t.(g t,f <g t, mem-mk-set(g;t)>)>
Date html generated:
2018_07_29-AM-10_09_01
Last ObjectModification:
2018_07_18-PM-05_04_25
Theory : constructive!set!theory
Home
Index