### Nuprl Lemma : range-sup-property

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

Proof

Definitions occuring in Statement :  range-sup: `sup{f[x]|x ∈ I}` continuous: `f[x] continuous for x ∈ I` rrange: `f[x](x∈I)` icompact: `icompact(I)` rfun: `I ⟶ℝ` interval: `Interval` sup: `sup(A) = b` so_apply: `x[s]` all: `∀x:A. B[x]` set: `{x:A| B[x]} `
Definitions unfolded in proof :  pi1: `fst(t)` r-ap: `f(x)` exists: `∃x:A. B[x]` squash: `↓T` sq_stable: `SqStable(P)` uimplies: `b supposing a` rfun: `I ⟶ℝ` label: `...\$L... t` prop: `ℙ` implies: `P `` Q` so_lambda: `λ2x.t[x]` uall: `∀[x:A]. B[x]` subtype_rel: `A ⊆r B` member: `t ∈ T` range-sup: `sup{f[x]|x ∈ I}` all: `∀x:A. B[x]` so_apply: `x[s]`
Lemmas referenced :  subtype_rel_function interval_wf set_wf equal_wf i-member_wf real_wf rfun_wf icompact_wf sq_stable__i-member r-ap_wf rrange_wf sup_wf exists_wf continuous_wf all_wf subtype_rel_self sup-range
Rules used in proof :  productElimination functionExtensionality equalitySymmetry equalityTransitivity setEquality dependent_set_memberEquality imageElimination baseClosed imageMemberEquality independent_functionElimination dependent_functionElimination independent_isectElimination hypothesisEquality lambdaEquality rename setElimination because_Cache functionEquality isectElimination sqequalHypSubstitution introduction hypothesis extract_by_obid instantiate thin applyEquality cut lambdaFormation computationStep sqequalTransitivity sqequalReflexivity sqequalRule sqequalSubstitution

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

Date html generated: 2018_05_22-PM-02_18_15
Last ObjectModification: 2018_05_21-AM-00_34_13

Theory : reals

Home Index