---

Step * 1 1 of Lemma Inorm-non-neg


1. I : {I:Interval| icompact(I)} 
2. f : I ⟶ℝ
3. mc : f[x] continuous for x ∈ I
4. |f[x]|(x∈I) ≤ sup{|f[x]||x ∈ I}
5. ∀e:ℝ. ((r0 < e) ⇒ (∃x:ℝ. ((x ∈ |f[x]|(x∈I)) ∧ ((sup{|f[x]||x ∈ I} - e) < x))))
6. icompact(I)
⊢ r0 ≤ sup{|f[x]||x ∈ I}
BY
{ (D -1 THEN Thin (-1) THEN D -1 THEN (D -4 With ⌜|f[r]|⌝  THENA Auto)) }

1
1. I : {I:Interval| icompact(I)} 
2. f : I ⟶ℝ
3. mc : f[x] continuous for x ∈ I
4. ∀e:ℝ. ((r0 < e) ⇒ (∃x:ℝ. ((x ∈ |f[x]|(x∈I)) ∧ ((sup{|f[x]||x ∈ I} - e) < x))))
5. r : ℝ
6. r ∈ I
7. (|f[r]| ∈ |f[x]|(x∈I)) ⇒ (|f[r]| ≤ sup{|f[x]||x ∈ I})
⊢ r0 ≤ sup{|f[x]||x ∈ I}

---

Latex:

---

Latex:

1.  I  :  \{I:Interval|  icompact(I)\} 
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  mc  :  f[x]  continuous  for  x  \mmember{}  I
4.  |f[x]|(x\mmember{}I)  \mleq{}  sup\{|f[x]||x  \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))))
6.  icompact(I)
\mvdash{}  r0  \mleq{}  sup\{|f[x]||x  \mmember{}  I\}


By

---

Latex:
(D  -1  THEN  Thin  (-1)  THEN  D  -1  THEN  (D  -4  With  \mkleeneopen{}|f[r]|\mkleeneclose{}    THENA  Auto))

---

Home Index