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: a function: x:A ⟶ B[x] natural_number: $n equal: 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: t ∈ T select: L[n] apply: 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