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