Nuprl Definition : interleaved_family
interleaved_family(T;I;L;L2) == ∃f:i:I ⟶ ℕ||L i|| ⟶ ℕ||L2||. interleaved_family_occurence(T;I;L;L2;f)
Definitions occuring in Statement :
interleaved_family_occurence: interleaved_family_occurence(T;I;L;L2;f),
length: ||as||,
int_seg: {i..j-},
exists: ∃x:A. B[x],
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],
apply: f a,
int_seg: {i..j-},
natural_number: $n,
length: ||as||,
interleaved_family_occurence: interleaved_family_occurence(T;I;L;L2;f)
FDL editor aliases :
interleaved_family
Latex:
interleaved\_family(T;I;L;L2) ==
\mexists{}f:i:I {}\mrightarrow{} \mBbbN{}||L i|| {}\mrightarrow{} \mBbbN{}||L2||. interleaved\_family\_occurence(T;I;L;L2;f)
Date html generated:
2016_05_15-PM-02_04_01
Last ObjectModification:
2015_09_23-AM-07_37_43
Theory : list!
Home
Index