---

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


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))))
BY
{ (InstLemma `function-on-compact` [⌜r0⌝;⌜r1⌝;⌜F⌝;⌜n⌝]⋅ THENA 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 : ℕ+
6. x : {t:ℝ| t ∈ [r0, r1]} 
7. y : {t:ℝ| t ∈ [r0, r1]} 
8. x = y
⊢ F[x] = F[y]

2
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 : ℕ+
6. ∃d:ℝ [((r0 < d) ∧ (∀x,y:ℝ.  ((x ∈ [r0, r1]) ⇒ (y ∈ [r0, r1]) ⇒ (|x - y| ≤ d) ⇒ (|F[x] - F[y]| ≤ (r1/r(n))))))]
⊢ ∃m:ℕ+. ((|t - (r1/r(2))| ≤ (r1/r(m))) ⇒ (|F(t)| ≤ (r1/r(n))))

---

Latex:

---

Latex:

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


By

---

Latex:
(InstLemma  `function-on-compact`  [\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}r1\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index