### Nuprl Lemma : int-rational

[n:ℤ]. (n ∈ ℚ)

Proof

Definitions occuring in Statement :  rationals: uall: [x:A]. B[x] member: t ∈ T int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B squash: T prop: true: True uimplies: supposing a guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q rationals: so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] all: x:A. B[x]
Lemmas referenced :  b-union_wf int_nzero_wf equal-wf-T-base bool_wf qeq_wf qeq-equiv subtype_rel_b-union-left equal_wf squash_wf true_wf qeq_refl btrue_wf iff_weakening_equal quotient-member-eq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry intEquality extract_by_obid isectElimination thin productEquality lambdaEquality hypothesisEquality baseClosed applyEquality because_Cache imageElimination natural_numberEquality imageMemberEquality universeEquality independent_isectElimination productElimination independent_functionElimination dependent_functionElimination

Latex:
\mforall{}[n:\mBbbZ{}].  (n  \mmember{}  \mBbbQ{})

Date html generated: 2018_05_21-PM-11_44_08
Last ObjectModification: 2017_07_26-PM-06_42_59

Theory : rationals

Home Index