Nuprl Lemma : functions-equal-on-interior
∀a:ℝ. ∀b:{b:ℝ| a < b} . ∀f,g:[a, b] ⟶ℝ.
((∀x,y:{x:ℝ| x ∈ [a, b]} . ((x = y) ⇒ (f(x) = f(y))))
⇒ (∀x,y:{x:ℝ| x ∈ [a, b]} . ((x = y) ⇒ (g(x) = g(y))))
⇒ (∀x:{x:ℝ| x ∈ (a, b)} . (f(x) = g(x)))
⇒ (∀x:{x:ℝ| x ∈ [a, b]} . (f(x) = g(x))))
Proof
Definitions occuring in Statement :
r-ap: f(x),
rfun: I ⟶ℝ,
rooint: (l, u),
rccint: [l, u],
i-member: r ∈ I,
rless: x < y,
req: x = y,
real: ℝ,
all: ∀x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]}
Definitions unfolded in proof :
rooint: (l, u),
rccint: [l, u],
i-member: r ∈ I,
so_apply: x[s],
so_lambda: λ2x.t[x],
prop: ℙ,
uimplies: b supposing a,
guard: {T},
uall: ∀[x:A]. B[x],
cand: A c∧ B,
and: P ∧ Q,
implies: P ⇒ Q,
top: Top,
member: t ∈ T,
subinterval: I ⊆ J ,
all: ∀x:A. B[x],
squash: ↓T,
sq_stable: SqStable(P),
or: P ∨ Q,
rneq: x ≠ y,
exists: ∃x:A. B[x]
Lemmas referenced :
rfun_wf,
r-ap_wf,
req_wf,
rooint_wf,
all_wf,
rccint_wf,
i-member_wf,
set_wf,
real_wf,
rless_wf,
rleq_weakening_rless,
member_rccint_lemma,
member_rooint_lemma,
interior-dense-in-interval,
functions-equal-on-dense,
exists_wf,
rneq_wf,
sq_stable__rless,
rleq_wf,
rleq_weakening_equal
Rules used in proof :
functionEquality,
independent_functionElimination,
because_Cache,
setEquality,
lambdaEquality,
productEquality,
rename,
setElimination,
independent_pairFormation,
independent_isectElimination,
hypothesisEquality,
isectElimination,
productElimination,
hypothesis,
voidEquality,
voidElimination,
isect_memberEquality,
thin,
dependent_functionElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
sqequalRule,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
imageElimination,
baseClosed,
imageMemberEquality,
inlFormation,
dependent_set_memberEquality,
dependent_pairFormation
Latex:
\mforall{}a:\mBbbR{}. \mforall{}b:\{b:\mBbbR{}| a < b\} . \mforall{}f,g:[a, b] {}\mrightarrow{}\mBbbR{}.
((\mforall{}x,y:\{x:\mBbbR{}| x \mmember{} [a, b]\} . ((x = y) {}\mRightarrow{} (f(x) = f(y))))
{}\mRightarrow{} (\mforall{}x,y:\{x:\mBbbR{}| x \mmember{} [a, b]\} . ((x = y) {}\mRightarrow{} (g(x) = g(y))))
{}\mRightarrow{} (\mforall{}x:\{x:\mBbbR{}| x \mmember{} (a, b)\} . (f(x) = g(x)))
{}\mRightarrow{} (\mforall{}x:\{x:\mBbbR{}| x \mmember{} [a, b]\} . (f(x) = g(x))))
Date html generated:
2017_10_03-AM-10_21_38
Last ObjectModification:
2017_07_31-PM-00_22_43
Theory : reals
Home
Index