Nuprl Definition : bag-inject
bag-inject(A;b;B;f) == Inj({x:A| x ↓∈ b} ;B;f)
Definitions occuring in Statement :
bag-member: x ↓∈ bs,
inject: Inj(A;B;f),
set: {x:A| B[x]}
Definitions occuring in definition :
inject: Inj(A;B;f),
set: {x:A| B[x]} ,
bag-member: x ↓∈ bs
FDL editor aliases :
bag-inject
Latex:
bag-inject(A;b;B;f) == Inj(\{x:A| x \mdownarrow{}\mmember{} b\} ;B;f)
Date html generated:
2016_05_15-PM-02_41_59
Last ObjectModification:
2015_09_23-AM-07_39_59
Theory : bags
Home
Index