Nuprl Definition : finite-nat-seq
finite-nat-seq() == n:ℕ × (ℕn ⟶ ℕ)
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],
function: x:A ⟶ B[x],
int_seg: {i..j-},
natural_number: $n,
nat: ℕ
FDL editor aliases :
finite-nat-seq
Latex:
finite-nat-seq() == n:\mBbbN{} \mtimes{} (\mBbbN{}n {}\mrightarrow{} \mBbbN{})
Date html generated:
2016_05_14-PM-09_54_23
Last ObjectModification:
2016_01_15-AM-07_32_28
Theory : continuity
Home
Index