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