Nuprl Definition : free-1-iso
free-1-iso(s;K) == <λx.Σ(p∈x). let k,s = p in k * 1, λk.{<* k 1, s>}, λb.Ax, λa.Ax>
Definitions occuring in Statement :
one-dim-vs: one-dim-vs(K),
vs-mul: a * x,
infix_ap: x f y,
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
axiom: Ax,
rng_one: 1,
rng_times: *,
rng_zero: 0,
rng_plus: +r,
bag-summation: Σ(x∈b). f[x],
single-bag: {x}
Definitions occuring in definition :
bag-summation: Σ(x∈b). f[x],
rng_zero: 0,
infix_ap: x f y,
rng_plus: +r,
spread: spread def,
vs-mul: a * x,
one-dim-vs: one-dim-vs(K),
single-bag: {x},
apply: f a,
rng_times: *,
rng_one: 1,
pair: <a, b>,
lambda: λx.A[x],
axiom: Ax
FDL editor aliases :
free-1-iso
Latex:
free-1-iso(s;K) == <\mlambda{}x.\mSigma{}(p\mmember{}x). let k,s = p in k * 1, \mlambda{}k.\{<* k 1, s>\}, \mlambda{}b.Ax, \mlambda{}a.Ax>
Date html generated:
2019_10_31-AM-06_30_53
Last ObjectModification:
2019_08_02-PM-04_35_22
Theory : linear!algebra
Home
Index