Nuprl Lemma : int_inc_rationals
ℤ ⊆r ℚ
Proof
Definitions occuring in Statement :
rationals: ℚ,
subtype_rel: A ⊆r B,
int: ℤ
Definitions unfolded in proof :
subtype_rel: A ⊆r B,
member: t ∈ T
Lemmas referenced :
int-subtype-rationals
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaEquality,
cut,
hypothesisEquality,
applyEquality,
thin,
introduction,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
sqequalRule,
intEquality
Latex:
\mBbbZ{} \msubseteq{}r \mBbbQ{}
Date html generated:
2019_10_16-AM-11_46_57
Last ObjectModification:
2018_09_17-PM-06_29_46
Theory : rationals
Home
Index