Nuprl Definition : single-valued-bag
single-valued-bag(b;T) == ∀x,y:T. (x ↓∈ b ⇒ y ↓∈ b ⇒ (x = y ∈ T))
Definitions occuring in Statement :
bag-member: x ↓∈ bs,
all: ∀x:A. B[x],
implies: P ⇒ Q,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
implies: P ⇒ Q,
bag-member: x ↓∈ bs,
equal: s = t ∈ T
FDL editor aliases :
single-valued-bag
Latex:
single-valued-bag(b;T) == \mforall{}x,y:T. (x \mdownarrow{}\mmember{} b {}\mRightarrow{} y \mdownarrow{}\mmember{} b {}\mRightarrow{} (x = y))
Date html generated:
2016_05_15-PM-02_42_16
Last ObjectModification:
2015_09_23-AM-07_40_07
Theory : bags
Home
Index