Nuprl Definition : embeddable
embeddable(R;L1;L2) == ∃f:ℕ||L1|| ⟶ ℕ||L2||. (increasing(f;||L1||) ∧ (∀j:ℕ||L1||. (R L1[j] L2[f j])))
Definitions occuring in Statement :
select: L[n],
length: ||as||,
increasing: increasing(f;k),
int_seg: {i..j-},
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 :
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
and: P ∧ Q,
increasing: increasing(f;k),
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
length: ||as||,
select: L[n],
apply: f a
FDL editor aliases :
embeddable
Latex:
embeddable(R;L1;L2) ==
\mexists{}f:\mBbbN{}||L1|| {}\mrightarrow{} \mBbbN{}||L2||. (increasing(f;||L1||) \mwedge{} (\mforall{}j:\mBbbN{}||L1||. (R L1[j] L2[f j])))
Date html generated:
2016_05_14-AM-07_44_38
Last ObjectModification:
2015_09_22-PM-05_53_57
Theory : list_1
Home
Index