### Nuprl Lemma : Inorm_wf

[I:{I:Interval| icompact(I)} ]. ∀[f:I ⟶ℝ]. ∀[mc:f[x] continuous for x ∈ I].  (||f[x]||_I ∈ ℝ)

Proof

Definitions occuring in Statement :  Inorm: ||f[x]||_I continuous: f[x] continuous for x ∈ I icompact: icompact(I) rfun: I ⟶ℝ interval: Interval real: uall: [x:A]. B[x] so_apply: x[s] member: t ∈ T set: {x:A| B[x]}
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T Inorm: ||f[x]||_I prop: so_lambda: λ2x.t[x] label: ...\$L... t rfun: I ⟶ℝ so_apply: x[s] subtype_rel: A ⊆B
Lemmas referenced :  range-sup_wf icompact_wf rabs_wf real_wf i-member_wf continuous-abs-subtype continuous_wf rfun_wf set_wf interval_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut setElimination thin rename sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination dependent_set_memberEquality because_Cache hypothesis hypothesisEquality lambdaEquality applyEquality setEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[I:\{I:Interval|  icompact(I)\}  ].  \mforall{}[f:I  {}\mrightarrow{}\mBbbR{}].  \mforall{}[mc:f[x]  continuous  for  x  \mmember{}  I].    (||f[x]||\_I  \mmember{}  \mBbbR{})

Date html generated: 2016_05_18-AM-09_17_06
Last ObjectModification: 2015_12_27-PM-11_26_04

Theory : reals

Home Index