Nuprl Lemma : functions-equal-on-dense
∀I:Interval
∀[X:{a:ℝ| a ∈ I} ⟶ ℙ]
(dense-in-interval(I;X)
⇒ (∃u,v:{a:ℝ| a ∈ I} . u ≠ v)
⇒ (∀f,g:I ⟶ℝ.
((∀x,y:{x:ℝ| x ∈ I} . ((x = y) ⇒ (f(x) = f(y))))
⇒ (∀x,y:{x:ℝ| x ∈ I} . ((x = y) ⇒ (g(x) = g(y))))
⇒ (∀x:{x:ℝ| x ∈ I} . ((X x) ⇒ (f(x) = g(x))))
⇒ (∀a:{x:ℝ| x ∈ I} . (f(a) = g(a))))))
Proof
Definitions occuring in Statement :
dense-in-interval: dense-in-interval(I;X),
r-ap: f(x),
rfun: I ⟶ℝ,
i-member: r ∈ I,
interval: Interval,
rneq: x ≠ y,
req: x = y,
real: ℝ,
uall: ∀[x:A]. B[x],
prop: ℙ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
squash: ↓T,
sq_stable: SqStable(P),
uimplies: b supposing a,
subtype_rel: A ⊆r B,
prop: ℙ,
and: P ∧ Q,
exists: ∃x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
r-ap: f(x),
so_apply: x[s],
rfun: I ⟶ℝ,
so_lambda: λ2x.t[x],
guard: {T},
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q)
Latex:
\mforall{}I:Interval
\mforall{}[X:\{a:\mBbbR{}| a \mmember{} I\} {}\mrightarrow{} \mBbbP{}]
(dense-in-interval(I;X)
{}\mRightarrow{} (\mexists{}u,v:\{a:\mBbbR{}| a \mmember{} I\} . u \mneq{} v)
{}\mRightarrow{} (\mforall{}f,g:I {}\mrightarrow{}\mBbbR{}.
((\mforall{}x,y:\{x:\mBbbR{}| x \mmember{} I\} . ((x = y) {}\mRightarrow{} (f(x) = f(y))))
{}\mRightarrow{} (\mforall{}x,y:\{x:\mBbbR{}| x \mmember{} I\} . ((x = y) {}\mRightarrow{} (g(x) = g(y))))
{}\mRightarrow{} (\mforall{}x:\{x:\mBbbR{}| x \mmember{} I\} . ((X x) {}\mRightarrow{} (f(x) = g(x))))
{}\mRightarrow{} (\mforall{}a:\{x:\mBbbR{}| x \mmember{} I\} . (f(a) = g(a))))))
Date html generated:
2020_05_20-PM-00_11_42
Last ObjectModification:
2019_12_28-AM-11_08_32
Theory : reals
Home
Index