---

Step * of Lemma rational-IVT-2

∀a,b:ℤ × ℕ+. ∀f:(ℤ × ℕ+) ⟶ (ℤ × ℕ+).
  ∀[g:{x:ℝ| x ∈ [ratreal(a), ratreal(b)]}  ⟶ ℝ]
    ∃c:{c:ℝ| c ∈ [ratreal(a), ratreal(b)]}  [(g[c] = r0)] 
    supposing (ratreal(a) ≤ ratreal(b))
    ∧ (ratreal(f[a]) ≤ r0)
    ∧ (r0 ≤ ratreal(f[b]))
    ∧ (∀x,y:{x:ℝ| x ∈ [ratreal(a), ratreal(b)]} .  ((x = y) ⇒ (g[x] = g[y])))
    ∧ (∀r:ℤ × ℕ+. ((ratreal(r) ∈ [ratreal(a), ratreal(b)]) ⇒ (g[ratreal(r)] = ratreal(f[r]))))
BY
{ Extract of Obid: rational-IVT-1
  not unfolding  divide primrec ratreal ratadd ratmul ratsub rat-nat-div exp-ratio ratbound rsub int-to-real
  finishing with (Try (Fold `rational-fun-zero` 0) THEN Auto)
  normalizes to:
  
  λa,b,f. rational-fun-zero(f;a;b) }

---

Latex:

---

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


By

---

Latex:
...

---

Home Index