### Nuprl Lemma : range-sup_wf

`∀[I:{I:Interval| icompact(I)} ]. ∀[f:I ⟶ℝ]. ∀[mc:f[x] continuous for 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` 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 :  r-ap: `f(x)` squash: `↓T` implies: `P `` Q` sq_stable: `SqStable(P)` uimplies: `b supposing a` guard: `{T}` prop: `ℙ` all: `∀x:A. B[x]` rfun: `I ⟶ℝ` label: `...\$L... t` so_lambda: `λ2x.t[x]` exists: `∃x:A. B[x]` subtype_rel: `A ⊆r B` range-sup: `sup{f[x]|x ∈ I}` member: `t ∈ T` uall: `∀[x:A]. B[x]` so_apply: `x[s]`
Lemmas referenced :  equal_wf all_wf sup-range icompact_wf interval_wf set_wf rfun_wf subtype_rel_self continuous_wf sq_stable__i-member i-member_wf r-ap_wf rrange_wf sup_wf exists_wf real_wf pi1_wf_top
Rules used in proof :  functionExtensionality functionEquality instantiate isect_memberEquality equalitySymmetry equalityTransitivity axiomEquality imageElimination baseClosed imageMemberEquality independent_functionElimination independent_isectElimination setEquality dependent_functionElimination dependent_set_memberEquality hypothesisEquality lambdaFormation lambdaEquality because_Cache applyEquality hypothesis isectElimination sqequalHypSubstitution extract_by_obid rename thin setElimination cut introduction isect_memberFormation 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\}  \mmember{}  \mBbbR{})

Date html generated: 2018_05_22-PM-02_18_01
Last ObjectModification: 2018_05_21-AM-00_33_36

Theory : reals

Home Index