Nuprl Lemma : equipollent-int-nat
ℤ ~ ℕ
Proof
Definitions occuring in Statement :
equipollent: A ~ B,
nat: ℕ,
int: ℤ
Definitions unfolded in proof :
equipollent: A ~ B
Lemmas referenced :
biject-int-nat
Rules used in proof :
hypothesis,
extract_by_obid,
introduction,
cut,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mBbbZ{} \msim{} \mBbbN{}
Date html generated:
2017_09_29-PM-06_04_46
Last ObjectModification:
2017_09_04-AM-11_19_16
Theory : equipollence!!cardinality!
Home
Index