---

Step * of Lemma rational-IVT-ext

∀a,b:ℝ. ∀f:(ℤ × ℕ+) ⟶ (ℤ × ℕ+).
  ∀[g:{x:ℝ| x ∈ [a, b]}  ⟶ ℝ]
    ∃c:{c:ℝ| c ∈ (a, b)}  [(g[c] = r0)] 
    supposing (a < b)
    ∧ ((g[a] * g[b]) < r0)
    ∧ (∀x,y:{x:ℝ| x ∈ [a, b]} .  ((x = y) ⇒ (g[x] = g[y])))
    ∧ (∀r:ℤ × ℕ+. ((ratreal(r) ∈ [a, b]) ⇒ (g[ratreal(r)] = ratreal(f[r]))))
BY
{ Extract of Obid: rational-IVT
  not unfolding  band lt_int le_int ratadd ratmul ratsub rminus mu-ge rational-fun-zero
  finishing with (Fold `rational_fun_zero` 0 THEN Auto)
  normalizes to:
  
  λa,b,f. rational_fun_zero(f;a;b) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.  \mforall{}f:(\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{})  {}\mrightarrow{}  (\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}).
    \mforall{}[g:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}    {}\mrightarrow{}  \mBbbR{}]
        \mexists{}c:\{c:\mBbbR{}|  c  \mmember{}  (a,  b)\}    [(g[c]  =  r0)] 
        supposing  (a  <  b)
        \mwedge{}  ((g[a]  *  g[b])  <  r0)
        \mwedge{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .    ((x  =  y)  {}\mRightarrow{}  (g[x]  =  g[y])))
        \mwedge{}  (\mforall{}r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}.  ((ratreal(r)  \mmember{}  [a,  b])  {}\mRightarrow{}  (g[ratreal(r)]  =  ratreal(f[r]))))


By

---

Latex:
Extract  of  Obid:  rational-IVT
not  unfolding    band  lt\_int  le\_int  ratadd  ratmul  ratsub  rminus  mu-ge  rational-fun-zero
finishing  with  (Fold  `rational\_fun\_zero`  0  THEN  Auto)
normalizes  to:

\mlambda{}a,b,f.  rational\_fun\_zero(f;a;b)

---

Home Index