---

Step * 1 1 1 1 1 1 1 1 of Lemma real-path-comp-exists


1. t : {x:ℝ| x ∈ [r0, r1]} 
⊢ ∀F:[r0, r1] ⟶ℝ
    ((∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) ⇒ (F(x) = F(y))))
    ⇒ (F((r1/r(2))) = r0)
    ⇒ (∀n:ℕ+. ∃m:ℕ+. ((|t - (r1/r(2))| ≤ (r1/r(m))) ⇒ (|F(t)| ≤ (r1/r(n))))))
BY
{ Auto }

1
1. t : {x:ℝ| x ∈ [r0, r1]} 
2. F : [r0, r1] ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) ⇒ (F(x) = F(y)))
4. F((r1/r(2))) = r0
5. n : ℕ+
⊢ ∃m:ℕ+. ((|t - (r1/r(2))| ≤ (r1/r(m))) ⇒ (|F(t)| ≤ (r1/r(n))))

---

Latex:

---

Latex:

1.  t  :  \{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\} 
\mvdash{}  \mforall{}F:[r0,  r1]  {}\mrightarrow{}\mBbbR{}
        ((\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}  .    ((x  =  y)  {}\mRightarrow{}  (F(x)  =  F(y))))
        {}\mRightarrow{}  (F((r1/r(2)))  =  r0)
        {}\mRightarrow{}  (\mforall{}n:\mBbbN{}\msupplus{}.  \mexists{}m:\mBbbN{}\msupplus{}.  ((|t  -  (r1/r(2))|  \mleq{}  (r1/r(m)))  {}\mRightarrow{}  (|F(t)|  \mleq{}  (r1/r(n))))))


By

---

Latex:
Auto

---

Home Index