Nuprl Definition : set-image
set-image(f;b) == let T,g = b in <T, λt.(f <g t, mem-mk-set(g;t)>)>
Definitions occuring in Statement :
mem-mk-set: mem-mk-set(f;t),
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>,
lambda: λx.A[x],
spread: spread def
FDL editor aliases :
set-image
Latex:
set-image(f;b) == let T,g = b in <T, \mlambda{}t.(f <g t, mem-mk-set(g;t)>)>
Date html generated:
2018_07_29-AM-10_08_42
Last ObjectModification:
2018_07_18-PM-00_31_06
Theory : constructive!set!theory
Home
Index