Nuprl Definition : nat-star
ℕ* == {s:ℕ ⟶ ℕ| ∀i,j:ℕ. (0 < s i ⇒ 0 < s j ⇒ (i = j ∈ ℤ))}
Definitions occuring in Statement :
nat: ℕ,
less_than: a < b,
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
int: ℤ,
equal: s = t ∈ T,
apply: f a,
natural_number: $n,
less_than: a < b,
implies: P ⇒ Q,
nat: ℕ,
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
set: {x:A| B[x]}
FDL editor aliases :
nat-star
Latex:
\mBbbN{}* == \{s:\mBbbN{} {}\mrightarrow{} \mBbbN{}| \mforall{}i,j:\mBbbN{}. (0 < s i {}\mRightarrow{} 0 < s j {}\mRightarrow{} (i = j))\}
Date html generated:
2016_12_12-AM-09_24_05
Last ObjectModification:
2016_11_18-AM-09_56_57
Theory : continuity
Home
Index