Nuprl Lemma : sup-range-no-mc
sup-range is Bishop's theorem that the range of a continuous function
has a supremum. To apply that theorem we need a modulus of continuity for f.
Since we can prove Brouwer's theorem real-continuity1
that all functions on a proper interval are continuous,
we can prove this version of the theorem that does not require a
modulus of continuity.
We have to take some care to handle the general case where the interval
may not be proper.
The constructive content of this theorem will be terribly inefficient
since it will first construct a modulus of continuity (using bar recursion).
But, the constructive content of the original theorem of Bishop was already
very inefficient. We should think of the supremum as the "specification" of
a (well defined) real number, that one may be able to compute efficiently
by other means.
⋅
∀I:{I:Interval| icompact(I)} . ∀f:{f:I ⟶ℝ| ifun(f;I)} . ∃y:ℝ. sup(f(x)(x∈I)) = y
Proof
Definitions occuring in Statement :
ifun: ifun(f;I),
rrange: f[x](x∈I),
icompact: icompact(I),
r-ap: f(x),
rfun: I ⟶ℝ,
interval: Interval,
sup: sup(A) = b,
real: ℝ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
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,
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
prop: ℙ
Lemmas referenced :
sup-range,
ifun-continuous,
sq_stable__icompact,
rfun_wf,
ifun_wf,
interval_wf,
icompact_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
setElimination,
rename,
because_Cache,
hypothesis,
independent_functionElimination,
sqequalRule,
imageMemberEquality,
baseClosed,
imageElimination,
setIsType,
universeIsType,
isectElimination,
independent_isectElimination
Latex:
\mforall{}I:\{I:Interval| icompact(I)\} . \mforall{}f:\{f:I {}\mrightarrow{}\mBbbR{}| ifun(f;I)\} . \mexists{}y:\mBbbR{}. sup(f(x)(x\mmember{}I)) = y
Date html generated:
2019_10_30-AM-07_44_20
Last ObjectModification:
2019_10_10-AM-10_19_46
Theory : reals
Home
Index