Nuprl Lemma : int-subtype-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,
uall: ∀[x:A]. B[x]
Lemmas referenced :
int-rational
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaEquality,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
intEquality
Latex:
\mBbbZ{} \msubseteq{}r \mBbbQ{}
Date html generated:
2016_05_15-PM-10_36_55
Last ObjectModification:
2015_12_27-PM-08_00_53
Theory : rationals
Home
Index