---

Step * 1 1 1 of Lemma Inorm-bound

.....antecedent..... 
1. I : {I:Interval| icompact(I)} 
2. f : I ⟶ℝ
3. mc : f[x] continuous for x ∈ I
4. x : {r:ℝ| r ∈ I} 
5. ∀e:ℝ. ((r0 < e) ⇒ (∃x:ℝ. ((x ∈ |f[x]|(x∈I)) ∧ ((sup{|f[x]||x ∈ I} - e) < x))))
⊢ |f[x]| ∈ |f[x]|(x∈I)
BY
{ (InstLemma `rset-member-rrange` [⌜I⌝;⌜λ2x.|f[x]|⌝]⋅ THEN Auto THEN BHyp -1  THEN Auto)⋅ }

---

Latex:

---

Latex:
.....antecedent..... 
1.  I  :  \{I:Interval|  icompact(I)\} 
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  mc  :  f[x]  continuous  for  x  \mmember{}  I
4.  x  :  \{r:\mBbbR{}|  r  \mmember{}  I\} 
5.  \mforall{}e:\mBbbR{}.  ((r0  <  e)  {}\mRightarrow{}  (\mexists{}x:\mBbbR{}.  ((x  \mmember{}  |f[x]|(x\mmember{}I))  \mwedge{}  ((sup\{|f[x]||x  \mmember{}  I\}  -  e)  <  x))))
\mvdash{}  |f[x]|  \mmember{}  |f[x]|(x\mmember{}I)


By

---

Latex:
(InstLemma  `rset-member-rrange`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.|f[x]|\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  BHyp  -1    THEN  Auto)\mcdot{}

---

Home Index