---

Step * of 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)))))))))
BY
{ (InstLemma `IVT-strict-decreasing` []
   THEN RepeatFor 4 ((ParallelLast' THENA Auto))
   THEN Auto
   THEN (Assert ∀x:{x:ℝ| x ∈ J} . ∃c:{x:ℝ| x ∈ I} . ((f c) = x) BY
               (((ParallelLast THENM ExRepD) THENA Auto)
                THEN (InstHyp [⌜a⌝;⌜b⌝;⌜x⌝] 5⋅ THENM ParallelLast)
                THEN Auto
                THEN InstLemma `i-member-between` [⌜I⌝;⌜a⌝;⌜b⌝]⋅
                THEN Auto))) }

1
1. I : Interval
2. f : I ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ I} .  ((x < y) ⇒ ((f y) < (f x)))
4. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))
5. ∀a,b:{x:ℝ| x ∈ I} .  ((a < b) ⇒ (∀x:ℝ. ((((f b) ≤ x) ∧ (x ≤ (f a))) ⇒ (∃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 b) ≤ x) ∧ (x ≤ (f a)))
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 y) < (g x))))
   ∧ (∀x,y:{t:ℝ| t ∈ J} .  ((x = y) ⇒ ((g x) = (g y)))))

---

Latex:

---

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)))))))))


By

---

Latex:
(InstLemma  `IVT-strict-decreasing`  []
  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto))
  THEN  Auto
  THEN  (Assert  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  J\}  .  \mexists{}c:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  ((f  c)  =  x)  BY
                          (((ParallelLast  THENM  ExRepD)  THENA  Auto)
                            THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  5\mcdot{}  THENM  ParallelLast)
                            THEN  Auto
                            THEN  InstLemma  `i-member-between`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
                            THEN  Auto)))

---

Home Index