Nuprl Definition : tree-big
tree-big(T;A;n) == ∀as:T List. ((||as|| = n ∈ ℤ) ⇒ (A as))
Definitions occuring in Statement :
length: ||as||,
list: T List,
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
list: T List,
implies: P ⇒ Q,
equal: s = t ∈ T,
int: ℤ,
length: ||as||,
apply: f a
FDL editor aliases :
tree-big
Latex:
tree-big(T;A;n) == \mforall{}as:T List. ((||as|| = n) {}\mRightarrow{} (A as))
Date html generated:
2016_05_14-PM-04_10_05
Last ObjectModification:
2015_09_22-PM-06_02_19
Theory : fan-theorem
Home
Index