Nuprl Definition : rationals
ℚ == r,s:ℤ ⋃ (ℤ × ℤ-o)//qeq(r;s) = tt
Definitions occuring in Statement :
qeq: qeq(r;s),
quotient: x,y:A//B[x; y],
int_nzero: ℤ-o,
b-union: A ⋃ B,
btrue: tt,
bool: 𝔹,
product: x:A × B[x],
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
quotient: x,y:A//B[x; y],
b-union: A ⋃ B,
product: x:A × B[x],
int: ℤ,
int_nzero: ℤ-o,
equal: s = t ∈ T,
bool: 𝔹,
qeq: qeq(r;s),
btrue: tt
FDL editor aliases :
rationals
Latex:
\mBbbQ{} == r,s:\mBbbZ{} \mcup{} (\mBbbZ{} \mtimes{} \mBbbZ{}\msupminus{}\msupzero{})//qeq(r;s) = tt
Date html generated:
2016_05_15-PM-10_36_50
Last ObjectModification:
2015_09_23-AM-08_26_50
Theory : rationals
Home
Index