Nuprl Definition : almost_full
almost_full(T;n;R) == ∀f:ℕ ⟶ T. ∃s:ℕn ⟶ ℕ. (strictly-increasing-seq(n;s) ∧ (R (f o s)))
Definitions occuring in Statement :
compose: f o g,
strictly-increasing-seq: strictly-increasing-seq(n;s),
int_seg: {i..j-},
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
int_seg: {i..j-},
natural_number: $n,
nat: ℕ,
and: P ∧ Q,
strictly-increasing-seq: strictly-increasing-seq(n;s),
apply: f a,
compose: f o g
FDL editor aliases :
almost_full
Latex:
almost\_full(T;n;R) == \mforall{}f:\mBbbN{} {}\mrightarrow{} T. \mexists{}s:\mBbbN{}n {}\mrightarrow{} \mBbbN{}. (strictly-increasing-seq(n;s) \mwedge{} (R (f o s)))
Date html generated:
2016_05_14-PM-04_08_09
Last ObjectModification:
2015_09_22-PM-06_02_10
Theory : fan-theorem
Home
Index