Nuprl Lemma : proper-continuous-implies
∀[I:Interval]. ∀[f:I ⟶ℝ].
(f[x] (proper)continuous for x ∈ I
⇒ (∀m:ℕ+. (icompact(i-approx(I;m)) ⇒ iproper(i-approx(I;m)) ⇒ f[x] continuous for x ∈ i-approx(I;m))))
Proof
Definitions occuring in Statement :
proper-continuous: f[x] (proper)continuous for x ∈ I,
continuous: f[x] continuous for x ∈ I,
icompact: icompact(I),
rfun: I ⟶ℝ,
i-approx: i-approx(I;n),
iproper: iproper(I),
interval: Interval,
nat_plus: ℕ+,
uall: ∀[x:A]. B[x],
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
all: ∀x:A. B[x],
proper-continuous: f[x] (proper)continuous for x ∈ I,
member: t ∈ T,
and: P ∧ Q,
prop: ℙ,
continuous: f[x] continuous for x ∈ I,
so_lambda: λ2x.t[x],
so_apply: x[s],
label: ...$L... t,
rfun: I ⟶ℝ,
top: Top
Lemmas referenced :
icompact_wf,
i-approx_wf,
iproper_wf,
set_wf,
nat_plus_wf,
proper-continuous_wf,
i-member_wf,
real_wf,
rfun_wf,
interval_wf,
i-approx-approx
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
dependent_set_memberEquality,
hypothesisEquality,
independent_pairFormation,
hypothesis,
productEquality,
cut,
introduction,
extract_by_obid,
isectElimination,
sqequalRule,
lambdaEquality,
applyEquality,
setElimination,
rename,
setEquality,
isect_memberEquality,
voidElimination,
voidEquality
Latex:
\mforall{}[I:Interval]. \mforall{}[f:I {}\mrightarrow{}\mBbbR{}].
(f[x] (proper)continuous for x \mmember{} I
{}\mRightarrow{} (\mforall{}m:\mBbbN{}\msupplus{}
(icompact(i-approx(I;m))
{}\mRightarrow{} iproper(i-approx(I;m))
{}\mRightarrow{} f[x] continuous for x \mmember{} i-approx(I;m))))
Date html generated:
2016_10_26-AM-09_43_29
Last ObjectModification:
2016_09_05-AM-10_03_16
Theory : reals
Home
Index