Nuprl Definition : finite
finite(T) == ∃n:ℕ. T ~ ℕn
Definitions occuring in Statement :
equipollent: A ~ B,
int_seg: {i..j-},
nat: ℕ,
exists: ∃x:A. B[x],
natural_number: $n
Definitions occuring in definition :
natural_number: $n,
int_seg: {i..j-},
equipollent: A ~ B,
nat: ℕ,
exists: ∃x:A. B[x]
FDL editor aliases :
finite
Latex:
finite(T) == \mexists{}n:\mBbbN{}. T \msim{} \mBbbN{}n
Date html generated:
2016_10_21-AM-11_00_03
Last ObjectModification:
2016_08_06-PM-02_33_35
Theory : equipollence!!cardinality!
Home
Index