Nuprl Definition : ubar
ubar(T;X) == ∃k:ℕ. ∀f:ℕ ⟶ T. ∃n:ℕk. (X map(f;upto(n)))
Definitions occuring in Statement :
upto: upto(n),
map: map(f;as),
int_seg: {i..j-},
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
nat: ℕ,
exists: ∃x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
apply: f a,
map: map(f;as),
upto: upto(n)
FDL editor aliases :
ubar
Latex:
ubar(T;X) == \mexists{}k:\mBbbN{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} T. \mexists{}n:\mBbbN{}k. (X map(f;upto(n)))
Date html generated:
2016_05_14-PM-04_09_15
Last ObjectModification:
2015_09_22-PM-06_02_15
Theory : fan-theorem
Home
Index