Nuprl Definition : bm_compare
bm_compare(K) ==
{compare:K ─→ K ─→ ℤ|
Trans(K;x,y.0 ≤ (compare x y))
∧ AntiSym(K;x,y.0 ≤ (compare x y))
∧ Connex(K;x,y.0 ≤ (compare x y))
∧ Refl(K;x,y.(compare x y) = 0 ∈ ℤ)
∧ Sym(K;x,y.(compare x y) = 0 ∈ ℤ)}
Definitions occuring in Statement :
connex: Connex(T;x,y.R[x; y])
,
anti_sym: AntiSym(T;x,y.R[x; y])
,
trans: Trans(T;x,y.E[x; y])
,
sym: Sym(T;x,y.E[x; y])
,
refl: Refl(T;x,y.E[x; y])
,
le: A ≤ B
,
and: P ∧ Q
,
set: {x:A| B[x]}
,
apply: f a
,
function: x:A ─→ B[x]
,
natural_number: $n
,
int: ℤ
,
equal: s = t ∈ T
FDL editor aliases :
bm_compare
bm\_compare(K) ==
\{compare:K {}\mrightarrow{} K {}\mrightarrow{} \mBbbZ{}|
Trans(K;x,y.0 \mleq{} (compare x y))
\mwedge{} AntiSym(K;x,y.0 \mleq{} (compare x y))
\mwedge{} Connex(K;x,y.0 \mleq{} (compare x y))
\mwedge{} Refl(K;x,y.(compare x y) = 0)
\mwedge{} Sym(K;x,y.(compare x y) = 0)\}
Date html generated:
2015_07_17-AM-08_19_21
Last ObjectModification:
2012_08_28-AM-11_55_58
Home
Index