Nuprl Definition : finite-type
finite-type(T) == ∃n:ℕ. ∃f:ℕn ⟶ T. Surj(ℕn;T;f)
Definitions occuring in Statement :
surject: Surj(A;B;f),
int_seg: {i..j-},
nat: ℕ,
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
nat: ℕ,
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
surject: Surj(A;B;f),
int_seg: {i..j-},
natural_number: $n
FDL editor aliases :
finite-type
Latex:
finite-type(T) == \mexists{}n:\mBbbN{}. \mexists{}f:\mBbbN{}n {}\mrightarrow{} T. Surj(\mBbbN{}n;T;f)
Date html generated:
2016_05_14-PM-01_50_22
Last ObjectModification:
2015_09_22-PM-05_54_53
Theory : list_1
Home
Index