Nuprl Definition : member-filter-witness
member-filter-witness(P;L;x) == λt.let i,_ = t in <filter-index(P;L) i, ⋅, ⋅>
Definitions occuring in Statement :
filter-index: filter-index(P;L),
it: ⋅,
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>
Definitions occuring in definition :
lambda: λx.A[x],
spread: spread def,
apply: f a,
filter-index: filter-index(P;L),
pair: <a, b>,
it: ⋅
FDL editor aliases :
member-filter-witness
Latex:
member-filter-witness(P;L;x) == \mlambda{}t.let i,$_{}$ = t in <filter-index(P;L) i, \mcdot{}, \000C\mcdot{}>
Date html generated:
2016_05_14-AM-07_50_56
Last ObjectModification:
2015_09_22-PM-05_54_06
Theory : list_1
Home
Index