Nuprl Definition : real-ss
ℝ == Point=ℝ #=λx,y. x ≠ y cotrans=TERMOF{rneq-cotrans:o, 1:l}
Definitions occuring in Statement :
mk-ss: Point=P #=Sep cotrans=C,
rneq: x ≠ y,
real: ℝ,
lambda: λx.A[x]
Definitions occuring in definition :
mk-ss: Point=P #=Sep cotrans=C,
real: ℝ,
lambda: λx.A[x],
rneq: x ≠ y,
rneq-cotrans
TermOfs occuring in Definition :
rneq-cotrans
FDL editor aliases :
real-ss
Latex:
\mBbbR{} == Point=\mBbbR{} \#=\mlambda{}x,y. x \mneq{} y cotrans=TERMOF\{rneq-cotrans:o, 1:l\}
Date html generated:
2019_10_31-AM-07_27_12
Last ObjectModification:
2019_09_19-PM-04_13_11
Theory : constructive!algebra
Home
Index