Nuprl Lemma : assert-rat-term-eq2

[r1,r2:rat_term()]. ∀[f:ℤ ⟶ ℝ].
  ((snd(rat_term_to_real(f;r1))) (snd(rat_term_to_real(f;r2)))) supposing 
     ((fst(rat_term_to_real(f;r1))) and 
     (fst(rat_term_to_real(f;r2))) and 
     (inl Ax ≤ rat-term-eq(r1;r2)))


Definitions occuring in Statement :  rat-term-eq: rat-term-eq(r1;r2) rat_term_to_real: rat_term_to_real(f;t) rat_term: rat_term() req: y real: uimplies: supposing a uall: [x:A]. B[x] pi1: fst(t) pi2: snd(t) function: x:A ⟶ B[x] inl: inl x int: sqle: s ≤ t axiom: Ax
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T all: x:A. B[x] implies:  Q pi2: snd(t) subtype_rel: A ⊆B prop: pi1: fst(t) and: P ∧ Q sq_stable: SqStable(P) squash: T it: btrue: tt mono: mono(T) is-above: is-above(T;a;z) exists: x:A. B[x] cand: c∧ B sq_type: SQType(T) guard: {T} assert: b ifthenelse: if then else fi  true: True
Lemmas referenced :  sq_stable__req uimplies_subtype real_wf assert-rat-term-eq rat_term_to_real_wf istype-sqle rat-term-eq_wf bool_subtype_base istype-int rat_term_wf bool-mono btrue_wf bool_wf subtype_base_sq req_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache inhabitedIsType hypothesis lambdaFormation_alt productElimination sqequalRule hypothesisEquality applyEquality independent_isectElimination hyp_replacement equalitySymmetry dependent_set_memberEquality_alt independent_pairFormation equalityTransitivity productIsType equalityIstype applyLambdaEquality setElimination rename lambdaEquality_alt universeIsType dependent_functionElimination independent_functionElimination imageMemberEquality baseClosed imageElimination functionIsType dependent_pairFormation_alt sqequalBase instantiate cumulativity natural_numberEquality

\mforall{}[r1,r2:rat\_term()].  \mforall{}[f:\mBbbZ{}  {}\mrightarrow{}  \mBbbR{}].
    ((snd(rat\_term\_to\_real(f;r1)))  =  (snd(rat\_term\_to\_real(f;r2))))  supposing 
          ((fst(rat\_term\_to\_real(f;r1)))  and 
          (fst(rat\_term\_to\_real(f;r2)))  and 
          (inl  Ax  \mleq{}  rat-term-eq(r1;r2)))

Date html generated: 2019_10_29-AM-09_54_19
Last ObjectModification: 2019_04_01-PM-07_02_46

Theory : reals

Home Index