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:Interval| icompact(I)} 
2. I ⟶ℝ
3. mc f[x] continuous for x ∈ I
4. {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