Nuprl Lemma : derivative_unique

[I:Interval]
(iproper(I)  (∀[f,g1,g2:I ⟶ℝ].  (d(f[x])/dx = λx.g1[x] on  d(f[x])/dx = λx.g2[x] on  rfun-eq(I;g1;g2))))

Proof

Definitions occuring in Statement :  derivative: d(f[x])/dx = λz.g[z] on I rfun-eq: rfun-eq(I;f;g) rfun: I ⟶ℝ iproper: iproper(I) interval: Interval uall: [x:A]. B[x] so_apply: x[s] implies:  Q
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  Q rfun-eq: rfun-eq(I;f;g) all: x:A. B[x] uimplies: supposing a sq_stable: SqStable(P) squash: T iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q prop: so_lambda: λ2x.t[x] so_apply: x[s] label: ...\$L... t rfun: I ⟶ℝ nat_plus: + rneq: x ≠ y guard: {T} or: P ∨ Q decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top derivative: d(f[x])/dx = λz.g[z] on I less_than: a < b less_than': less_than'(a;b) true: True sq_exists: x:{A| B[x]} rless: x < y cand: c∧ B subinterval: I ⊆  rev_uimplies: rev_uimplies(P;Q) rge: x ≥ y itermConstant: "const" req_int_terms: t1 ≡ t2 uiff: uiff(P;Q) r-ap: f(x) rdiv: (x/y) subtype_rel: A ⊆B
Lemmas referenced :  req-iff-rabs-rleq r-ap_wf sq_stable__i-member nat_plus_wf set_wf real_wf i-member_wf derivative_wf req_witness rfun_wf iproper_wf interval_wf sq_stable__rleq rabs_wf rsub_wf rdiv_wf int-to-real_wf rless-int nat_plus_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf rless_wf i-member-proper-iff i-approx-compact mul_nat_plus less_than_wf icompact_wf i-approx_wf compact-proper-interval-near-member rleq_wf rmin_strict_ub rmin_wf i-approx-is-subinterval rmin_ub rleq_functionality_wrt_implies rmul_wf itermMultiply_wf int_term_value_mul_lemma rleq_weakening_equal rleq_weakening real_term_polynomial itermSubtract_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_mul_lemma real_term_value_var_lemma req-iff-rsub-is-0 rleq_functionality rabs-difference-symmetry req_weakening radd_wf equal_wf rminus_wf radd_functionality_wrt_rleq r-triangle-inequality req_functionality req_inversion rabs-rmul rabs_functionality itermAdd_wf itermMinus_wf real_term_value_add_lemma real_term_value_minus_lemma rmul-distrib1 req_wf rneq_functionality rmul-int rneq-int intformeq_wf int_formula_prop_eq_lemma equal-wf-T-base rinv_wf2 uiff_transitivity rmul_functionality rdiv_functionality rinv-of-rmul req_transitivity rmul-rinv3 rinv-mul-as-rdiv rmul_preserves_rleq squash_wf true_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isectElimination because_Cache hypothesisEquality setElimination rename hypothesis independent_isectElimination independent_functionElimination sqequalRule imageMemberEquality baseClosed imageElimination productElimination lambdaEquality applyEquality dependent_set_memberEquality setEquality isect_memberEquality natural_numberEquality inrFormation unionElimination dependent_pairFormation int_eqEquality intEquality voidElimination voidEquality independent_pairFormation computeAll addLevel levelHypothesis productEquality multiplyEquality equalityTransitivity equalitySymmetry functionEquality impliesFunctionality universeEquality

Latex:
\mforall{}[I:Interval]
(iproper(I)
{}\mRightarrow{}  (\mforall{}[f,g1,g2:I  {}\mrightarrow{}\mBbbR{}].
(d(f[x])/dx  =  \mlambda{}x.g1[x]  on  I  {}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.g2[x]  on  I  {}\mRightarrow{}  rfun-eq(I;g1;g2))))

Date html generated: 2017_10_03-PM-00_07_34
Last ObjectModification: 2017_07_28-AM-08_33_22

Theory : reals

Home Index