---

Step * of Lemma inverse-of-strict-monotonic-function

∀I:Interval. ∀f:I ⟶ℝ.
  (((∀x,y:{x:ℝ| x ∈ I} .  ((x < y) ⇒ ((f x) < (f y)))) ∨ (∀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 a) ≤ x) ∧ (x ≤ (f 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 x) < (g y)))) ∨ (∀x,y:{x:ℝ| x ∈ J} .  ((x < y) ⇒ ((g y) < (g x)))\000C))
             ∧ (∀x,y:{t:ℝ| t ∈ J} .  ((x = y) ⇒ ((g x) = (g y)))))))))
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN (D -2
         THENL [(InstLemma `inverse-of-strict-increasing-function-exists` [⌜I⌝;⌜f⌝]⋅ THENA Auto)
               ; (InstLemma `inverse-of-strict-decreasing-function-exists` [⌜I⌝;⌜f⌝]⋅ THENA Auto)]
   )
   THEN RepeatFor 4 (ParallelLast)
   THEN Auto
   THEN ExRepD
   THEN D -2
   THEN D -1
   THEN Try ((Assert ⌜False⌝⋅ THEN Auto THEN FHyp 3 [-3] THEN Complete (Auto)))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.
    (((\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  <  y)  {}\mRightarrow{}  ((f  x)  <  (f  y))))
      \mvee{}  (\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  \mneq{}  b  \mwedge{}  ((((f  a)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  (f  b)))  \mvee{}  (((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  x)  <  (g  y))))
                              \mvee{}  (\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)))))))))


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  (D  -2
              THENL  [(InstLemma  `inverse-of-strict-increasing-function-exists`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
                          ;  (InstLemma  `inverse-of-strict-decreasing-function-exists`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)]
  )
  THEN  RepeatFor  4  (ParallelLast)
  THEN  Auto
  THEN  ExRepD
  THEN  D  -2
  THEN  D  -1
  THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  FHyp  3  [-3]  THEN  Complete  (Auto)))
  THEN  Auto)

---

Home Index