Nuprl Definition : similar-bags
similar-bags(A;as;bs) == ∀a:A. (a ↓∈ as ∧ 0 < #(bs) ⇐⇒ a ↓∈ bs ∧ 0 < #(as))
Definitions occuring in Statement :
bag-member: x ↓∈ bs,
bag-size: #(bs),
less_than: a < b,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
bag-member: x ↓∈ bs,
less_than: a < b,
natural_number: $n,
bag-size: #(bs)
FDL editor aliases :
similar-bags
Latex:
similar-bags(A;as;bs) == \mforall{}a:A. (a \mdownarrow{}\mmember{} as \mwedge{} 0 < \#(bs) \mLeftarrow{}{}\mRightarrow{} a \mdownarrow{}\mmember{} bs \mwedge{} 0 < \#(as))
Date html generated:
2016_05_15-PM-02_42_08
Last ObjectModification:
2015_09_23-AM-07_40_03
Theory : bags
Home
Index