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

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


Proof




Definitions occuring in Statement :  rfun: I ⟶ℝ i-member: r ∈ I interval: Interval rless: x < y req: y real: all: 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 :  rfun: I ⟶ℝ so_apply: x[s] so_lambda: λ2x.t[x] uall: [x:A]. B[x] prop: member: t ∈ T cand: c∧ B and: P ∧ Q implies:  Q all: x:A. B[x] guard: {T} false: False or: P ∨ Q rneq: x ≠ y not: ¬A uimplies: supposing a subtype_rel: A ⊆B rev_implies:  Q iff: ⇐⇒ Q squash: T sq_stable: SqStable(P) subinterval: I ⊆  top: Top real-fun: real-fun(f;a;b) real-sfun: real-sfun(f;a;b) rev_uimplies: rev_uimplies(P;Q) uiff: uiff(P;Q)
Lemmas referenced :  rfun_wf interval_wf all_wf req_wf rless_wf i-member_wf real_wf set_wf rneq_wf rless_irreflexivity rleq_weakening rless_transitivity1 req_inversion not-rneq rleq_weakening_rless rless_transitivity2 rless_functionality not-rless rleq_wf rcc-subinterval equal_wf sq_stable__i-member rccint_wf rfun_subtype real-fun-implies-sfun member_rccint_lemma subtype_rel_sets rleq_weakening_equal req_functionality
Rules used in proof :  functionEquality dependent_set_memberEquality functionExtensionality applyEquality setEquality because_Cache rename setElimination independent_pairFormation hypothesisEquality lambdaEquality sqequalRule hypothesis thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution dependent_functionElimination voidElimination independent_functionElimination unionElimination independent_isectElimination productElimination equalitySymmetry equalityTransitivity imageElimination baseClosed imageMemberEquality voidEquality isect_memberEquality inlFormation productEquality

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



Date html generated: 2017_10_03-AM-10_32_40
Last ObjectModification: 2017_07_30-AM-11_46_50

Theory : reals


Home Index