Nuprl Definition : l_intersection
l_intersection(eq;L1;L2) == filter(λx.x ∈b L2;L1)
Definitions occuring in Statement :
deq-member: x ∈b L,
filter: filter(P;l),
lambda: λx.A[x]
Definitions occuring in definition :
filter: filter(P;l),
lambda: λx.A[x],
deq-member: x ∈b L
FDL editor aliases :
l_intersection
Latex:
l\_intersection(eq;L1;L2) == filter(\mlambda{}x.x \mmember{}\msubb{} L2;L1)
Date html generated:
2016_05_14-PM-03_32_25
Last ObjectModification:
2015_09_22-PM-06_00_53
Theory : decidable!equality
Home
Index