Nuprl Definition : is-path
is-path(A;f) == ∀n:ℕ. (A map(f;upto(n)))
Definitions occuring in Statement :
upto: upto(n),
map: map(f;as),
nat: ℕ,
all: ∀x:A. B[x],
apply: f a
Definitions occuring in definition :
all: ∀x:A. B[x],
nat: ℕ,
apply: f a,
map: map(f;as),
upto: upto(n)
FDL editor aliases :
is-path
Latex:
is-path(A;f) == \mforall{}n:\mBbbN{}. (A map(f;upto(n)))
Date html generated:
2016_05_14-PM-04_09_50
Last ObjectModification:
2015_09_22-PM-06_02_17
Theory : fan-theorem
Home
Index