Nuprl Definition : cardinality-le
|T| ≤ n == ∃f:ℕn ⟶ T. Surj(ℕn;T;f)
Definitions occuring in Statement :
surject: Surj(A;B;f),
int_seg: {i..j-},
exists: ∃x:A. B[x],
function: x:A ⟶ B[x],
natural_number: $n
Definitions occuring in definition :
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 :
cardinality-le
Latex:
|T| \mleq{} n == \mexists{}f:\mBbbN{}n {}\mrightarrow{} T. Surj(\mBbbN{}n;T;f)
Date html generated:
2016_05_14-PM-01_51_28
Last ObjectModification:
2015_09_22-PM-05_54_57
Theory : list_1
Home
Index