### Nuprl 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)`

Proof

Definitions occuring in Statement :  Inorm: `||f[x]||_I` continuous: `f[x] continuous for x ∈ I` icompact: `icompact(I)` rfun: `I ⟶ℝ` i-member: `r ∈ I` interval: `Interval` rleq: `x ≤ y` rabs: `|x|` real: `ℝ` uall: `∀[x:A]. B[x]` so_apply: `x[s]` set: `{x:A| B[x]} `
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` rleq: `x ≤ y` rnonneg: `rnonneg(x)` all: `∀x:A. B[x]` le: `A ≤ B` and: `P ∧ Q` not: `¬A` implies: `P `` Q` false: `False` so_lambda: `λ2x.t[x]` label: `...\$L... t` rfun: `I ⟶ℝ` so_apply: `x[s]` prop: `ℙ` subtype_rel: `A ⊆r B` Inorm: `||f[x]||_I` sup: `sup(A) = b` upper-bound: `A ≤ b` sq_stable: `SqStable(P)` squash: `↓T`
Lemmas referenced :  sq_stable__i-member rset-member-rrange continuous-abs-subtype range-sup-property icompact_wf interval_wf rfun_wf continuous_wf set_wf nat_plus_wf rabs_wf i-member_wf real_wf Inorm_wf rsub_wf less_than'_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality productElimination independent_pairEquality because_Cache lemma_by_obid isectElimination applyEquality setEquality hypothesis setElimination rename minusEquality natural_numberEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality voidElimination independent_functionElimination imageMemberEquality baseClosed imageElimination

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)

Date html generated: 2016_05_18-AM-09_17_20
Last ObjectModification: 2016_01_17-AM-02_40_10

Theory : reals

Home Index