Nuprl Definition : bag-order
bag-order(T) ==
{cmp:bag(T) ⟶ bag(T) ⟶ ℤ|
(∀as,bs:bag(T). (((cmp as bs) = 0 ∈ ℤ
⇐⇒ as = bs ∈ bag(T)) ∧ (cmp as bs < 0
⇐⇒ (cmp bs as) > 0)))
∧ Linorder(bag(T);as,bs.(cmp as bs) ≤ 0)}
Definitions occuring in Statement :
bag: bag(T)
,
linorder: Linorder(T;x,y.R[x; y])
,
less_than: a < b
,
gt: i > j
,
le: A ≤ B
,
all: ∀x:A. B[x]
,
iff: P
⇐⇒ Q
,
and: P ∧ Q
,
set: {x:A| B[x]}
,
apply: f a
,
function: x:A ⟶ B[x]
,
natural_number: $n
,
int: ℤ
,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]}
,
function: x:A ⟶ B[x]
,
all: ∀x:A. B[x]
,
and: P ∧ Q
,
int: ℤ
,
equal: s = t ∈ T
,
iff: P
⇐⇒ Q
,
less_than: a < b
,
gt: i > j
,
linorder: Linorder(T;x,y.R[x; y])
,
bag: bag(T)
,
le: A ≤ B
,
apply: f a
,
natural_number: $n
FDL editor aliases :
bag-order
Latex:
bag-order(T) ==
\{cmp:bag(T) {}\mrightarrow{} bag(T) {}\mrightarrow{} \mBbbZ{}|
(\mforall{}as,bs:bag(T). (((cmp as bs) = 0 \mLeftarrow{}{}\mRightarrow{} as = bs) \mwedge{} (cmp as bs < 0 \mLeftarrow{}{}\mRightarrow{} (cmp bs as) > 0)))
\mwedge{} Linorder(bag(T);as,bs.(cmp as bs) \mleq{} 0)\}
Date html generated:
2016_05_15-PM-03_11_09
Last ObjectModification:
2015_09_23-AM-07_42_17
Theory : bags
Home
Index