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