Nuprl Definition : nat-inf
ℕ∞ == {f:ℕ ⟶ 𝔹| ∀n:ℕ. ((↑(f (n + 1))) ⇒ (↑(f n)))}
Definitions occuring in Statement :
nat: ℕ,
assert: ↑b,
bool: 𝔹,
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
bool: 𝔹,
all: ∀x:A. B[x],
nat: ℕ,
implies: P ⇒ Q,
add: n + m,
natural_number: $n,
assert: ↑b,
apply: f a
FDL editor aliases :
nat-inf
Latex:
\mBbbN{}\minfty{} == \{f:\mBbbN{} {}\mrightarrow{} \mBbbB{}| \mforall{}n:\mBbbN{}. ((\muparrow{}(f (n + 1))) {}\mRightarrow{} (\muparrow{}(f n)))\}
Date html generated:
2016_05_15-PM-01_46_44
Last ObjectModification:
2015_09_23-AM-07_37_07
Theory : basic
Home
Index