---

Step * of Lemma near-fixpoint-on-0-1

No Annotations
∀f:[r0, r1] ⟶ℝ
  ((∀x:ℝ. ((x ∈ [r0, r1]) ⇒ (f[x] ∈ [r0, r1])))
  ⇒ f[x] continuous for x ∈ [r0, r1]
  ⇒ (∀e:ℝ. ((r0 < e) ⇒ (∃x:ℝ. ((x ∈ [r0, r1]) ∧ (|f[x] - x| < e))))))
BY
{ (Auto THEN (InstLemma `rless-cases` [⌜r0⌝;⌜e⌝;⌜f[r0]⌝]⋅ THENA Auto) THEN D -1) }

1
1. f : [r0, r1] ⟶ℝ
2. ∀x:ℝ. ((x ∈ [r0, r1]) ⇒ (f[x] ∈ [r0, r1]))
3. f[x] continuous for x ∈ [r0, r1]
4. e : ℝ
5. r0 < e
6. r0 < f[r0]
⊢ ∃x:ℝ. ((x ∈ [r0, r1]) ∧ (|f[x] - x| < e))

2
1. f : [r0, r1] ⟶ℝ
2. ∀x:ℝ. ((x ∈ [r0, r1]) ⇒ (f[x] ∈ [r0, r1]))
3. f[x] continuous for x ∈ [r0, r1]
4. e : ℝ
5. r0 < e
6. f[r0] < e
⊢ ∃x:ℝ. ((x ∈ [r0, r1]) ∧ (|f[x] - x| < e))

---

Latex:

---

Latex:
No  Annotations
\mforall{}f:[r0,  r1]  {}\mrightarrow{}\mBbbR{}
    ((\mforall{}x:\mBbbR{}.  ((x  \mmember{}  [r0,  r1])  {}\mRightarrow{}  (f[x]  \mmember{}  [r0,  r1])))
    {}\mRightarrow{}  f[x]  continuous  for  x  \mmember{}  [r0,  r1]
    {}\mRightarrow{}  (\mforall{}e:\mBbbR{}.  ((r0  <  e)  {}\mRightarrow{}  (\mexists{}x:\mBbbR{}.  ((x  \mmember{}  [r0,  r1])  \mwedge{}  (|f[x]  -  x|  <  e))))))


By

---

Latex:
(Auto  THEN  (InstLemma  `rless-cases`  [\mkleeneopen{}r0\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}f[r0]\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index