Nuprl Lemma : near-inverse-of-increasing-function

∀f:ℝ ⟶ ℝ. ∀n,M:ℕ+. ∀z:ℝ. ∀a,b:ℤ.
  ∀k:ℕ+
    (∃c:ℤ. (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])) supposing 
       ((z ≤ f[(r(b))/k]) and 
       (f[(r(a))/k] ≤ z) and 
       (∀x,y:ℝ.
          (((r(a))/k ≤ x)
          ⇒ (x < y)
          ⇒ (y ≤ (r(b))/k)
          ⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n)))))))) 
  supposing a < b


Proof



Definitions occuring in Statement :  rdiv: (x/y),  rleq: x ≤ y,  rless: x < y,  rabs: |x|,  int-rdiv: (a)/k1,  rsub: x - y,  int-to-real: r(n),  real: ℝ,  nat_plus: ℕ+,  less_than: a < b,  uimplies: b supposing a,  so_apply: x[s],  all: ∀x:A. B[x],  sq_exists: ∃x:A [B[x]],  exists: ∃x:A. B[x],  implies: P ⇒ Q,  and: P ∧ Q,  function: x:A ⟶ B[x],  natural_number: $n,  int: ℤ
Definitions unfolded in proof :  all: ∀x:A. B[x],  member: t ∈ T,  uall: ∀[x:A]. B[x],  so_lambda: λ2x.t[x],  uimplies: b supposing a,  prop: ℙ,  nat_plus: ℕ+,  nat: ℕ,  implies: P ⇒ Q,  subtype_rel: A ⊆r B,  and: P ∧ Q,  so_apply: x[s],  rneq: x ≠ y,  guard: {T},  or: P ∨ Q,  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  rless: x < y,  sq_exists: ∃x:A [B[x]],  ge: i ≥ j ,  decidable: Dec(P),  not: ¬A,  satisfiable_int_formula: satisfiable_int_formula(fmla),  exists: ∃x:A. B[x],  false: False,  top: Top,  le: A ≤ B,  rleq: x ≤ y,  rnonneg: rnonneg(x),  int_seg: {i..j-},  lelt: i ≤ j < k,  less_than: a < b,  squash: ↓T,  rdiv: (x/y),  uiff: uiff(P;Q),  req_int_terms: t1 ≡ t2,  true: True,  rev_uimplies: rev_uimplies(P;Q),  cand: A c∧ B,  rge: x ≥ y,  int_nzero: ℤ-o,  nequal: a ≠ b ∈ T ,  sq_type: SQType(T),  real: ℝ,  sq_stable: SqStable(P)
Lemmas referenced :  real_wf,  nat_plus_wf,  uniform-comp-nat-induction,  all_wf,  isect_wf,  less_than_wf,  le_wf,  subtract_wf,  rleq_wf,  int-rdiv_wf,  nat_plus_inc_int_nzero,  int-to-real_wf,  rless_wf,  rsub_wf,  rdiv_wf,  rless-int,  nat_plus_properties,  nat_properties,  decidable__lt,  full-omega-unsat,  intformand_wf,  intformnot_wf,  intformless_wf,  itermConstant_wf,  itermVar_wf,  istype-int,  int_formula_prop_and_lemma,  istype-void,  int_formula_prop_not_lemma,  int_formula_prop_less_lemma,  int_term_value_constant_lemma,  int_term_value_var_lemma,  int_formula_prop_wf,  exists_wf,  sq_exists_wf,  rabs_wf,  istype-le,  istype-less_than,  istype-nat,  member-less_than,  le_witness_for_triv,  decidable__le,  int_seg_wf,  int_seg_properties,  itermMultiply_wf,  itermSubtract_wf,  rinv_wf2,  rmul_wf,  rmul_preserves_rless,  rleq_weakening_equal,  rless_functionality,  int-rdiv-req,  req_transitivity,  rmul_functionality,  req_weakening,  rmul-rinv,  req-iff-rsub-is-0,  real_polynomial_null,  real_term_value_sub_lemma,  real_term_value_mul_lemma,  real_term_value_var_lemma,  real_term_value_const_lemma,  int_term_value_subtract_lemma,  int_term_value_minus_lemma,  int_term_value_add_lemma,  int_term_value_mul_lemma,  int_formula_prop_le_lemma,  intformle_wf,  rleq-int-fractions2,  itermMinus_wf,  itermAdd_wf,  rminus_wf,  radd_wf,  rmul_preserves_rleq,  rleq_functionality,  rsub_functionality,  radd_functionality,  rminus_functionality,  squash_wf,  true_wf,  rminus-int,  radd-int,  rinv-mul-as-rdiv,  real_term_value_add_lemma,  real_term_value_minus_lemma,  rleq-implies-rleq,  rleq_functionality_wrt_implies,  rabs-of-nonneg,  radd-preserves-rleq,  mul_preserves_lt,  rleq-int-fractions,  set-value-type,  equal_wf,  int-value-type,  nearby-cases,  intformeq_wf,  int_formula_prop_eq_lemma,  int_subtype_base,  nequal_wf,  rleq_weakening_rless,  subtype_base_sq,  decidable__equal_int,  sq_stable__less_than,  mul_preserves_le,  nat_plus_subtype_nat,  int-rdiv-cancel,  subtype_rel_self,  iff_weakening_equal
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  lambdaFormation_alt,  cut,  universeIsType,  introduction,  extract_by_obid,  hypothesis,  because_Cache,  functionIsType,  inhabitedIsType,  hypothesisEquality,  sqequalHypSubstitution,  isectElimination,  thin,  sqequalRule,  lambdaEquality_alt,  closedConclusion,  intEquality,  multiplyEquality,  setElimination,  rename,  functionEquality,  applyEquality,  productEquality,  natural_numberEquality,  independent_isectElimination,  inrFormation_alt,  dependent_functionElimination,  productElimination,  independent_functionElimination,  unionElimination,  approximateComputation,  dependent_pairFormation_alt,  int_eqEquality,  isect_memberEquality_alt,  voidElimination,  independent_pairFormation,  productIsType,  isect_memberFormation_alt,  equalityTransitivity,  equalitySymmetry,  independent_pairEquality,  functionIsTypeImplies,  isectIsType,  imageElimination,  setIsType,  minusEquality,  addEquality,  imageMemberEquality,  baseClosed,  dependent_set_memberFormation_alt,  cutEval,  dependent_set_memberEquality_alt,  equalityIstype,  sqequalBase,  instantiate,  cumulativity,  promote_hyp,  baseApply,  universeEquality
Latex:
\mforall{}f:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}n,M:\mBbbN{}\msupplus{}.  \mforall{}z:\mBbbR{}.  \mforall{}a,b:\mBbbZ{}.
    \mforall{}k:\mBbbN{}\msupplus{}
        (\mexists{}c:\mBbbZ{}
            (\mexists{}j:\mBbbN{}\msupplus{}  [((|f[(r(c))/j]  -  z|  \mleq{}  (r1/r(n)))
                          \mwedge{}  ((r(a))/k  \mleq{}  (r(c))/j)
                          \mwedge{}  ((r(c))/j  \mleq{}  (r(b))/k))]))  supposing 
              ((z  \mleq{}  f[(r(b))/k])  and 
              (f[(r(a))/k]  \mleq{}  z)  and 
              (\mforall{}x,y:\mBbbR{}.
                    (((r(a))/k  \mleq{}  x)
                    {}\mRightarrow{}  (x  <  y)
                    {}\mRightarrow{}  (y  \mleq{}  (r(b))/k)
                    {}\mRightarrow{}  ((f[x]  \mleq{}  f[y])  \mwedge{}  (((y  -  x)  \mleq{}  (r1/r(M)))  {}\mRightarrow{}  ((f[y]  -  f[x])  \mleq{}  (r1/r(n)))))))) 
    supposing  a  <  b


Date html generated: 2019_10_29-AM-10_06_47
Last ObjectModification: 2019_10_10-AM-10_23_54

Theory : reals


Home Index