Nuprl Definition : comparison
comparison(T) ==
{cmp:T ⟶ T ⟶ ℤ|
(∀x,y:T. ((cmp x y) = (-(cmp y x)) ∈ ℤ))
∧ (∀x,y:T. (((cmp x y) = 0 ∈ ℤ) ⇒ (∀z:T. ((cmp x z) = (cmp y z) ∈ ℤ))))
∧ (∀x,y,z:T. ((0 ≤ (cmp x y)) ⇒ (0 ≤ (cmp y z)) ⇒ (0 ≤ (cmp x z))))}
Definitions occuring in Statement :
le: A ≤ B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
minus: -n,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
minus: -n,
and: P ∧ Q,
equal: s = t ∈ T,
int: ℤ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
le: A ≤ B,
natural_number: $n,
apply: f a
FDL editor aliases :
comparison
Latex:
comparison(T) ==
\{cmp:T {}\mrightarrow{} T {}\mrightarrow{} \mBbbZ{}|
(\mforall{}x,y:T. ((cmp x y) = (-(cmp y x))))
\mwedge{} (\mforall{}x,y:T. (((cmp x y) = 0) {}\mRightarrow{} (\mforall{}z:T. ((cmp x z) = (cmp y z)))))
\mwedge{} (\mforall{}x,y,z:T. ((0 \mleq{} (cmp x y)) {}\mRightarrow{} (0 \mleq{} (cmp y z)) {}\mRightarrow{} (0 \mleq{} (cmp x z))))\}
Date html generated:
2016_05_14-PM-02_35_13
Last ObjectModification:
2015_09_22-PM-05_56_21
Theory : list_1
Home
Index