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