Nuprl Definition : nat
ℕ == {i:ℤ| 0 ≤ i}
Definitions occuring in Statement :
le: A ≤ B,
set: {x:A| B[x]} ,
natural_number: $n,
int: ℤ
Definitions occuring in definition :
set: {x:A| B[x]} ,
int: ℤ,
le: A ≤ B,
natural_number: $n
Rules referencing :
barInduction,
bar_Induction,
strong_bar_Induction,
Continuity,
StrongContinuity2,
compactness,
sqequalnReflexivity,
sqntypeEquality,
sqlenSubtypeRel,
sqequalDefinition,
sqleDefinition,
sqlenIntensionalEquality,
sqequalnIntensionalEquality,
fixpointLeast
FDL editor aliases :
nat
Latex:
\mBbbN{} == \{i:\mBbbZ{}| 0 \mleq{} i\}
Date html generated:
2016_05_13-PM-03_32_01
Last ObjectModification:
2015_09_22-PM-05_44_53
Theory : arithmetic
Home
Index