Nuprl Definition : consistent-seq
R-consistent-seq(n) == {s:ℕn ⟶ T| ∀x:ℕn. (R x s (s x))}
Definitions occuring in Statement :
int_seg: {i..j-},
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
apply: f a
FDL editor aliases :
consistent-seq
Latex:
R-consistent-seq(n) == \{s:\mBbbN{}n {}\mrightarrow{} T| \mforall{}x:\mBbbN{}n. (R x s (s x))\}
Date html generated:
2016_05_13-PM-03_48_44
Last ObjectModification:
2015_09_22-PM-05_45_18
Theory : bar-induction
Home
Index