Nuprl Lemma : equipollent-rationals-ext
ℚ ~ {p:ℤ × ℕ+| ↑is-qrep(p)}
Proof
Definitions occuring in Statement :
is-qrep: is-qrep(p),
rationals: ℚ,
equipollent: A ~ B,
nat_plus: ℕ+,
assert: ↑b,
set: {x:A| B[x]} ,
product: x:A × B[x],
int: ℤ
Definitions unfolded in proof :
member: t ∈ T,
equipollent-rationals,
assert-is-qrep,
sq_stable__assert
Lemmas referenced :
equipollent-rationals,
assert-is-qrep,
sq_stable__assert
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mBbbQ{} \msim{} \{p:\mBbbZ{} \mtimes{} \mBbbN{}\msupplus{}| \muparrow{}is-qrep(p)\}
Date html generated:
2018_05_21-PM-11_48_59
Last ObjectModification:
2018_05_19-PM-03_56_10
Theory : rationals
Home
Index