Nuprl Definition : cosetTC
cosetTC(a) == mk-coset({p:copath(T.T;a)| 0 < copath-length(p)} ;λp.copath-at(a;p))
Definitions occuring in Statement :
mk-coset: mk-coset(T;f),
copath-length: copath-length(p),
copath-at: copath-at(w;p),
copath: copath(a.B[a];w),
less_than: a < b,
set: {x:A| B[x]} ,
lambda: λx.A[x],
natural_number: $n
Definitions occuring in definition :
copath-at: copath-at(w;p),
lambda: λx.A[x],
copath-length: copath-length(p),
natural_number: $n,
less_than: a < b,
copath: copath(a.B[a];w),
set: {x:A| B[x]} ,
mk-coset: mk-coset(T;f)
FDL editor aliases :
cosetTC
Latex:
cosetTC(a) == mk-coset(\{p:copath(T.T;a)| 0 < copath-length(p)\} ;\mlambda{}p.copath-at(a;p))
Date html generated:
2018_07_29-AM-10_00_17
Last ObjectModification:
2018_07_18-PM-05_36_33
Theory : constructive!set!theory
Home
Index