Nuprl Definition : bag-disjoint
bag-disjoint(T;as;bs) == ∀x:T. (¬(x ↓∈ as ∧ x ↓∈ bs))
Definitions occuring in Statement :
bag-member: x ↓∈ bs,
all: ∀x:A. B[x],
not: ¬A,
and: P ∧ Q
Definitions occuring in definition :
all: ∀x:A. B[x],
not: ¬A,
and: P ∧ Q,
bag-member: x ↓∈ bs
FDL editor aliases :
bag-disjoint
Latex:
bag-disjoint(T;as;bs) == \mforall{}x:T. (\mneg{}(x \mdownarrow{}\mmember{} as \mwedge{} x \mdownarrow{}\mmember{} bs))
Date html generated:
2016_05_15-PM-02_44_13
Last ObjectModification:
2015_09_23-AM-07_40_14
Theory : bags
Home
Index