### Nuprl Lemma : qeq-qrep

`∀[r:ℚ]. qeq(r;qrep(r)) = tt`

Proof

Definitions occuring in Statement :  qrep: `qrep(r)` rationals: `ℚ` qeq: `qeq(r;s)` btrue: `tt` bool: `𝔹` uall: `∀[x:A]. B[x]` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` rationals: `ℚ` member: `t ∈ T` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` all: `∀x:A. B[x]` implies: `P `` Q` prop: `ℙ` b-union: `A ⋃ B` tunion: `⋃x:A.B[x]` bool: `𝔹` unit: `Unit` ifthenelse: `if b then t else f fi ` pi2: `snd(t)` qrep: `qrep(r)` qeq: `qeq(r;s)` uimplies: `b supposing a` callbyvalueall: callbyvalueall has-value: `(a)↓` has-valueall: `has-valueall(a)` btrue: `tt` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` int_nzero: `ℤ-o` bfalse: `ff` spreadn: spread3 it: `⋅` uiff: `uiff(P;Q)` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` le: `A ≤ B` squash: `↓T` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` nat: `ℕ` ge: `i ≥ j ` nequal: `a ≠ b ∈ T `
Lemmas referenced :  bool_wf b-union_wf int_nzero_wf equal_wf equal-wf-base equal-wf-T-base qeq_wf rationals_wf valueall-type-has-valueall int-valueall-type evalall-reduce product-valueall-type evalall-sqequal int_subtype_base set-valueall-type nequal_wf le_int_wf eqtt_to_assert assert_of_le_int eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot le_wf set_subtype_base eq_int_eq_true decidable__equal_int satisfiable-full-omega-tt intformnot_wf intformeq_wf itermMultiply_wf itermVar_wf itermConstant_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_mul_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_wf btrue_wf iff_weakening_equal gcd_reduce_property gcd_reduce_wf nat_wf squash_wf true_wf equal-wf-base-T coprime_wf nat_properties int_nzero_properties intformand_wf itermMinus_wf int_formula_prop_and_lemma int_term_value_minus_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation sqequalHypSubstitution pointwiseFunctionalityForEquality cut introduction extract_by_obid hypothesis sqequalRule pertypeElimination productElimination thin equalityTransitivity equalitySymmetry isectElimination intEquality productEquality lambdaFormation hypothesisEquality dependent_functionElimination independent_functionElimination because_Cache baseClosed imageElimination unionElimination equalityElimination independent_isectElimination callbyvalueReduce isintReduceTrue lambdaEquality independent_pairEquality natural_numberEquality baseApply closedConclusion applyEquality dependent_pairFormation promote_hyp instantiate cumulativity voidElimination minusEquality multiplyEquality int_eqEquality isect_memberEquality voidEquality computeAll imageMemberEquality universeEquality setElimination rename independent_pairFormation

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

Date html generated: 2018_05_21-PM-11_47_34
Last ObjectModification: 2017_07_26-PM-06_43_10

Theory : rationals

Home Index