---

Step * 1 of Lemma inverse-of-strict-increasing-function-exists


1. I : Interval
2. f : I ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ I} .  ((x < y) ⇒ ((f x) < (f y)))
4. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))
5. ∀a,b:{x:ℝ| x ∈ I} .  ((a < b) ⇒ (∀x:ℝ. ((((f a) ≤ x) ∧ (x ≤ (f b))) ⇒ (∃c:ℝ. (((a ≤ c) ∧ (c ≤ b)) ∧ ((f c) = x)))))\000C)
6. J : Interval
7. ∀t:{t:ℝ| t ∈ I} . (f t ∈ J)
8. ∀x:{x:ℝ| x ∈ J} . ∃a,b:{t:ℝ| t ∈ I} . ((a < b) ∧ ((f a) ≤ x) ∧ (x ≤ (f b)))
9. ∀x:{x:ℝ| x ∈ J} . ∃c:{x:ℝ| x ∈ I} . ((f c) = x)
⊢ ∃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 x) < (g y))))
   ∧ (∀x,y:{t:ℝ| t ∈ J} .  ((x = y) ⇒ ((g x) = (g y)))))
BY
{ ((Skolemize (-1) `g' THENA Auto)
   THEN (D 0 With ⌜g⌝  THENA Auto)
   THEN D 0
   THEN Try (Trivial)
   THEN InstLemma `inverse-of-strict-increasing-function` [⌜I⌝;⌜f⌝;⌜J⌝;⌜g⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  <  y)  {}\mRightarrow{}  ((f  x)  <  (f  y)))
4.  \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y)))
5.  \mforall{}a,b:\{x:\mBbbR{}|  x  \mmember{}  I\}  .
          ((a  <  b)
          {}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  ((((f  a)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  (f  b)))  {}\mRightarrow{}  (\mexists{}c:\mBbbR{}.  (((a  \mleq{}  c)  \mwedge{}  (c  \mleq{}  b))  \mwedge{}  ((f  c)  =  x))))))
6.  J  :  Interval
7.  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  I\}  .  (f  t  \mmember{}  J)
8.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  J\}  .  \mexists{}a,b:\{t:\mBbbR{}|  t  \mmember{}  I\}  .  ((a  <  b)  \mwedge{}  ((f  a)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  (f  b)))
9.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  J\}  .  \mexists{}c:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  ((f  c)  =  x)
\mvdash{}  \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  x)  <  (g  y))))
      \mwedge{}  (\mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  J\}  .    ((x  =  y)  {}\mRightarrow{}  ((g  x)  =  (g  y)))))


By

---

Latex:
((Skolemize  (-1)  `g'  THENA  Auto)
  THEN  (D  0  With  \mkleeneopen{}g\mkleeneclose{}    THENA  Auto)
  THEN  D  0
  THEN  Try  (Trivial)
  THEN  InstLemma  `inverse-of-strict-increasing-function`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index