Step
*
of Lemma
Inorm-bound
∀[I:{I:Interval| icompact(I)} ]. ∀[f:I ⟶ℝ]. ∀[mc:f[x] continuous for x ∈ I]. ∀[x:{r:ℝ| r ∈ I} ].  (|f[x]| ≤ ||f[x]||_I)
BY
{ Auto }
1
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
Latex:
Latex:
\mforall{}[I:\{I:Interval|  icompact(I)\}  ].  \mforall{}[f:I  {}\mrightarrow{}\mBbbR{}].  \mforall{}[mc:f[x]  continuous  for  x  \mmember{}  I].  \mforall{}[x:\{r:\mBbbR{}|  r  \mmember{}  I\}  ].
    (|f[x]|  \mleq{}  ||f[x]||\_I)
By
Latex:
Auto
Home
Index