Nuprl Definition : sequence
sequence(T) == k:ℕ × (ℕk ⟶ T)
Definitions occuring in Statement :
int_seg: {i..j-},
nat: ℕ,
function: x:A ⟶ B[x],
product: x:A × B[x],
natural_number: $n
Definitions occuring in definition :
product: x:A × B[x],
nat: ℕ,
function: x:A ⟶ B[x],
int_seg: {i..j-},
natural_number: $n
FDL editor aliases :
sequence
Latex:
sequence(T) == k:\mBbbN{} \mtimes{} (\mBbbN{}k {}\mrightarrow{} T)
Date html generated:
2018_07_25-PM-01_28_05
Last ObjectModification:
2018_06_11-PM-01_09_28
Theory : arithmetic
Home
Index