### Nuprl Lemma : sup-range

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

Proof

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

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

Date html generated: 2016_05_18-AM-09_15_30
Last ObjectModification: 2016_01_17-AM-02_37_53

Theory : reals

Home Index