Nuprl Lemma : inverse-of-strict-decreasing-function-exists

I:Interval. ∀f:I ⟶ℝ.
  ((∀x,y:{x:ℝx ∈ I} .  ((x < y)  ((f y) < (f x))))
   (∀x,y:{t:ℝt ∈ I} .  ((x y)  ((f x) (f y))))
   (∀J:Interval
        ((∀t:{t:ℝt ∈ I} (f t ∈ J))
         (∀x:{x:ℝx ∈ J} . ∃a,b:{t:ℝt ∈ I} ((a < b) ∧ ((f b) ≤ x) ∧ (x ≤ (f a))))
         (∃g:{x:ℝx ∈ J}  ⟶ {x:ℝx ∈ I} 
             ((∀x:{x:ℝx ∈ J} ((f (g x)) x))
             ∧ (∀x:{x:ℝx ∈ I} ((g (f x)) x))
             ∧ (∀x,y:{x:ℝx ∈ J} .  ((x < y)  ((g y) < (g x))))
             ∧ (∀x,y:{t:ℝt ∈ J} .  ((x y)  ((g x) (g y)))))))))


Proof




Definitions occuring in Statement :  rfun: I ⟶ℝ i-member: r ∈ I interval: Interval rleq: x ≤ y rless: x < y req: y real: all: x:A. B[x] exists: x:A. B[x] implies:  Q and: P ∧ Q set: {x:A| B[x]}  apply: a function: x:A ⟶ B[x]
Definitions unfolded in proof :  so_apply: x[s] so_lambda: λ2x.t[x] rfun: I ⟶ℝ prop: uall: [x:A]. B[x] squash: T sq_stable: SqStable(P) cand: c∧ B and: P ∧ Q exists: x:A. B[x] implies:  Q member: t ∈ T all: x:A. B[x] guard: {T} subtype_rel: A ⊆B pi1: fst(t)
Lemmas referenced :  rfun_wf interval_wf rleq_wf rless_wf exists_wf real_wf all_wf req_wf i-member_wf sq_stable__i-member i-member-between IVT-strict-decreasing inverse-of-strict-decreasing-function set_wf equal_wf
Rules used in proof :  functionEquality productEquality lambdaEquality setEquality applyEquality isectElimination because_Cache dependent_set_memberEquality imageElimination baseClosed imageMemberEquality sqequalRule dependent_pairFormation independent_pairFormation rename setElimination productElimination independent_functionElimination hypothesisEquality thin dependent_functionElimination sqequalHypSubstitution hypothesis lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution extract_by_obid introduction cut equalitySymmetry equalityTransitivity functionExtensionality promote_hyp

Latex:
\mforall{}I:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.
    ((\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  <  y)  {}\mRightarrow{}  ((f  y)  <  (f  x))))
    {}\mRightarrow{}  (\mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y))))
    {}\mRightarrow{}  (\mforall{}J:Interval
                ((\mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  I\}  .  (f  t  \mmember{}  J))
                {}\mRightarrow{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  J\}  .  \mexists{}a,b:\{t:\mBbbR{}|  t  \mmember{}  I\}  .  ((a  <  b)  \mwedge{}  ((f  b)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  (f  a))))
                {}\mRightarrow{}  (\mexists{}g:\{x:\mBbbR{}|  x  \mmember{}  J\}    {}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  I\} 
                          ((\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  J\}  .  ((f  (g  x))  =  x))
                          \mwedge{}  (\mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  ((g  (f  x))  =  x))
                          \mwedge{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  J\}  .    ((x  <  y)  {}\mRightarrow{}  ((g  y)  <  (g  x))))
                          \mwedge{}  (\mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  J\}  .    ((x  =  y)  {}\mRightarrow{}  ((g  x)  =  (g  y)))))))))



Date html generated: 2017_10_03-AM-10_33_36
Last ObjectModification: 2017_07_30-AM-11_57_37

Theory : reals


Home Index