Nuprl Definition : unbounded-list-predicate
Unbounded(A) == ∀n:ℕ. ∃as:T List. ((||as|| = n ∈ ℤ) ∧ (A as))
Definitions occuring in Statement :
length: ||as||,
list: T List,
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
nat: ℕ,
exists: ∃x:A. B[x],
list: T List,
and: P ∧ Q,
equal: s = t ∈ T,
int: ℤ,
length: ||as||,
apply: f a
FDL editor aliases :
unbounded-list-predicate
Latex:
Unbounded(A) == \mforall{}n:\mBbbN{}. \mexists{}as:T List. ((||as|| = n) \mwedge{} (A as))
Date html generated:
2016_05_14-PM-04_10_21
Last ObjectModification:
2015_09_22-PM-06_02_20
Theory : fan-theorem
Home
Index