### 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)))`

Proof

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: `x = y` real: `ℝ` uimplies: `b 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: `b supposing a` member: `t ∈ T` all: `∀x:A. B[x]` implies: `P `` Q` pi2: `snd(t)` subtype_rel: `A ⊆r 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: `A c∧ B` sq_type: `SQType(T)` guard: `{T}` assert: `↑b` ifthenelse: `if b then t else f 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

Latex:
\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