Nuprl Lemma : near-inverse-of-increasing-function-ext
∀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 :
member: t ∈ T,
subtract: n - m,
so_apply: x[s],
genrec-ap: genrec-ap,
near-inverse-of-increasing-function,
decidable__le,
uniform-comp-nat-induction,
nearby-cases,
decidable__and,
decidable__not,
decidable__less_than',
decidable__lt,
rleq_functionality_wrt_implies,
decidable__implies,
decidable__false,
any: any x,
decidable__squash,
decidable_functionality,
squash_elim,
sq_stable_from_decidable,
iff_preserves_decidability,
sq_stable__from_stable,
stable__from_decidable,
uall: ∀[x:A]. B[x],
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
so_apply: x[s1;s2;s3;s4],
so_lambda: λ2x.t[x],
top: Top,
uimplies: b supposing a
Lemmas referenced :
near-inverse-of-increasing-function,
lifting-strict-decide,
istype-void,
strict4-decide,
lifting-strict-less,
lifting-strict-callbyvalue,
decidable__le,
uniform-comp-nat-induction,
nearby-cases,
decidable__and,
decidable__not,
decidable__less_than',
decidable__lt,
rleq_functionality_wrt_implies,
decidable__implies,
decidable__false,
decidable__squash,
decidable_functionality,
squash_elim,
sq_stable_from_decidable,
iff_preserves_decidability,
sq_stable__from_stable,
stable__from_decidable
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry,
isectElimination,
baseClosed,
isect_memberEquality_alt,
voidElimination,
independent_isectElimination
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_07_00
Last ObjectModification:
2019_02_05-PM-04_47_42
Theory : reals
Home
Index