Nuprl Definition : sub-mset
sub-mset(T; L1; L2) == ∃L:T List. permutation(T;L @ L1;L2)
Definitions occuring in Statement :
permutation: permutation(T;L1;L2),
append: as @ bs,
list: T List,
exists: ∃x:A. B[x]
Definitions occuring in definition :
exists: ∃x:A. B[x],
list: T List,
permutation: permutation(T;L1;L2),
append: as @ bs
FDL editor aliases :
sub-mset
Latex:
sub-mset(T; L1; L2) == \mexists{}L:T List. permutation(T;L @ L1;L2)
Date html generated:
2016_05_15-PM-04_31_33
Last ObjectModification:
2015_09_23-AM-07_49_00
Theory : general
Home
Index