### Nuprl Lemma : equals-qrep

`∀[r:ℚ]. (qrep(r) = r ∈ ℚ)`

Proof

Definitions occuring in Statement :  qrep: `qrep(r)` rationals: `ℚ` uall: `∀[x:A]. B[x]` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` rationals: `ℚ` so_lambda: `λ2x y.t[x; y]` guard: `{T}` so_apply: `x[s1;s2]` uimplies: `b supposing a` implies: `P `` Q` pi2: `snd(t)` so_apply: `x[s]` so_lambda: `λ2x.t[x]` bfalse: `ff` ifthenelse: `if b then t else f fi ` tunion: `⋃x:A.B[x]` b-union: `A ⋃ B` istype: `istype(T)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` true: `True` prop: `ℙ` squash: `↓T` and: `P ∧ Q` quotient: `x,y:A//B[x; y]`
Lemmas referenced :  qeq_wf qeq-qrep subtype_quotient equal-wf-T-base bool_wf qeq-equiv qrep_wf quotient-member-eq b-union_wf int_nzero_wf rationals_wf ifthenelse_wf nat_plus_inc_int_nzero istype-int nat_plus_wf subtype_rel_product bfalse_wf quotient_wf equal_functionality_wrt_subtype_rel2 subtype_rel_self iff_weakening_equal istype-universe true_wf squash_wf equal_wf qeq_refl
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut introduction extract_by_obid lambdaFormation_alt sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality sqequalRule because_Cache lambdaEquality_alt hypothesis baseClosed inhabitedIsType independent_isectElimination equalitySymmetry dependent_functionElimination independent_functionElimination universeIsType intEquality productEquality universeEquality instantiate equalityTransitivity dependent_pairEquality_alt imageMemberEquality closedConclusion natural_numberEquality imageElimination productIsType productElimination pertypeElimination pointwiseFunctionality sqequalBase equalityIstype promote_hyp

Latex:
\mforall{}[r:\mBbbQ{}].  (qrep(r)  =  r)

Date html generated: 2019_10_16-AM-11_47_44
Last ObjectModification: 2019_06_25-PM-00_20_49

Theory : rationals

Home Index