---

Step * 1 of Lemma Inorm-bound


1. I : {I:Interval| icompact(I)} 
2. f : I ⟶ℝ
3. mc : f[x] continuous for x ∈ I
4. x : {r:ℝ| r ∈ I} 
⊢ |f[x]| ≤ ||f[x]||_I
BY
{ (Unfold `Inorm` 0 THEN (InstLemma `range-sup-property` [⌜I⌝;⌜λ2x.|f[x]|⌝;⌜mc⌝]⋅ THENA Auto)) }

1
1. I : {I:Interval| icompact(I)} 
2. f : I ⟶ℝ
3. mc : f[x] continuous for x ∈ I
4. x : {r:ℝ| r ∈ I} 
5. sup(|f[x]|(x∈I)) = sup{|f[x]||x ∈ I}
⊢ |f[x]| ≤ 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.  x  :  \{r:\mBbbR{}|  r  \mmember{}  I\} 
\mvdash{}  |f[x]|  \mleq{}  ||f[x]||\_I


By

---

Latex:
(Unfold  `Inorm`  0  THEN  (InstLemma  `range-sup-property`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.|f[x]|\mkleeneclose{};\mkleeneopen{}mc\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index