Nuprl Definition : real-ring
real-ring() == <x,y:ℝ//(x = y), λx,y. ff, λx,y. ff, λx,y. (x + y), r0, λx.-(x), λx,y. (x * y), r1, λx,y. (inr ⋅ )>
Definitions occuring in Statement :
req: x = y,
rmul: a * b,
rminus: -(x),
radd: a + b,
int-to-real: r(n),
real: ℝ,
quotient: x,y:A//B[x; y],
bfalse: ff,
it: ⋅,
lambda: λx.A[x],
pair: <a, b>,
inr: inr x ,
natural_number: $n
Definitions occuring in definition :
quotient: x,y:A//B[x; y],
real: ℝ,
req: x = y,
bfalse: ff,
radd: a + b,
rminus: -(x),
rmul: a * b,
pair: <a, b>,
int-to-real: r(n),
natural_number: $n,
lambda: λx.A[x],
inr: inr x ,
it: ⋅
FDL editor aliases :
real-ring
Latex:
real-ring() == <x,y:\mBbbR{}//(x = y), \mlambda{}x,y. ff, \mlambda{}x,y. ff, \mlambda{}x,y. (x + y), r0, \mlambda{}x.-(x), \mlambda{}x,y. (x * y), r1, \000C\mlambda{}x,y. (inr \mcdot{} )>
Date html generated:
2019_10_30-AM-08_09_21
Last ObjectModification:
2019_09_18-PM-03_37_45
Theory : reals
Home
Index