Nuprl Definition : sublist
L1 ⊆ L2 == ∃f:ℕ||L1|| ⟶ ℕ||L2||. (increasing(f;||L1||) ∧ (∀j:ℕ||L1||. (L1[j] = L2[f j] ∈ T)))
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,
equal: s = t ∈ T
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||,
equal: s = t ∈ T,
select: L[n],
apply: f a
FDL editor aliases :
sublist
Latex:
L1 \msubseteq{} L2 == \mexists{}f:\mBbbN{}||L1|| {}\mrightarrow{} \mBbbN{}||L2||. (increasing(f;||L1||) \mwedge{} (\mforall{}j:\mBbbN{}||L1||. (L1[j] = L2[f j])))
Date html generated:
2016_05_14-AM-07_42_52
Last ObjectModification:
2015_09_22-PM-05_53_57
Theory : list_1
Home
Index