Nuprl Definition : free-iso-int
free-iso-int(s) == <λx.Σ(p∈x). let k,s = p in k, λk.{<k, s>}, λb.Ax, λa.Ax>
Definitions occuring in Statement :
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
add: n + m,
natural_number: $n,
axiom: Ax,
bag-summation: Σ(x∈b). f[x],
single-bag: {x}
Definitions occuring in definition :
bag-summation: Σ(x∈b). f[x],
natural_number: $n,
add: n + m,
spread: spread def,
single-bag: {x},
pair: <a, b>,
lambda: λx.A[x],
axiom: Ax
FDL editor aliases :
free-iso-int
Latex:
free-iso-int(s) == <\mlambda{}x.\mSigma{}(p\mmember{}x). let k,s = p in k, \mlambda{}k.\{<k, s>\}, \mlambda{}b.Ax, \mlambda{}a.Ax>
Date html generated:
2019_10_31-AM-06_31_00
Last ObjectModification:
2019_08_02-PM-04_51_16
Theory : linear!algebra
Home
Index