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:  Q sq_stable: SqStable(P) uimplies: 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 ⊆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