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