Nuprl Lemma : real-path-comp-exists
∀f,g:[r0, r1] ⟶ℝ.
((∀x,y:{x:ℝ| x ∈ [r0, r1]} . ((x = y) ⇒ (f(x) = f(y))))
⇒ (∀x,y:{x:ℝ| x ∈ [r0, r1]} . ((x = y) ⇒ (g(x) = g(y))))
⇒ (f(r1) = g(r0))
⇒ (∃h:[r0, r1] ⟶ℝ
((∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (h(t) = f(r(2) * t)))
∧ (∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (h(t) = g((r(2) * t) - r1)))
∧ (∀x,y:{x:ℝ| x ∈ [r0, r1]} . ((x = y) ⇒ (h(x) = h(y)))))))
Proof
Definitions occuring in Statement :
r-ap: f(x),
rfun: I ⟶ℝ,
rccint: [l, u],
i-member: r ∈ I,
rdiv: (x/y),
rsub: x - y,
req: x = y,
rmul: a * b,
int-to-real: r(n),
real: ℝ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
natural_number: $n
Definitions unfolded in proof :
rev_uimplies: rev_uimplies(P;Q),
req_int_terms: t1 ≡ t2,
rdiv: (x/y),
rccint: [l, u],
i-member: r ∈ I,
uiff: uiff(P;Q),
exists: ∃x:A. B[x],
satisfiable_int_formula: satisfiable_int_formula(fmla),
decidable: Dec(P),
nat_plus: ℕ+,
not: ¬A,
false: False,
le: A ≤ B,
cand: A c∧ B,
sq_stable: SqStable(P),
prop: ℙ,
true: True,
less_than': less_than'(a;b),
squash: ↓T,
less_than: a < b,
rev_implies: P ⇐ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
or: P ∨ Q,
guard: {T},
rneq: x ≠ y,
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
all: ∀x:A. B[x],
r-ap: f(x),
so_apply: x[s],
sq_exists: ∃x:A [B[x]],
rless: x < y,
rfun: I ⟶ℝ,
rtermSubtract: left "-" right,
pi2: snd(t),
rtermDivide: num "/" denom,
rtermMultiply: left "*" right,
pi1: fst(t),
rat_term_ind: rat_term_ind,
rtermConstant: "const",
rat_term_to_real: rat_term_to_real(f;t),
so_lambda: λ2x.t[x],
subtype_rel: A ⊆r B,
cauchy: cauchy(n.x[n]),
ge: i ≥ j ,
nat: ℕ,
real: ℝ,
absval: |i|,
rge: x ≥ y,
converges-to: lim n→∞.x[n] = y,
rleq: x ≤ y,
rnonneg: rnonneg(x)
Latex:
\mforall{}f,g:[r0, r1] {}\mrightarrow{}\mBbbR{}.
((\mforall{}x,y:\{x:\mBbbR{}| x \mmember{} [r0, r1]\} . ((x = y) {}\mRightarrow{} (f(x) = f(y))))
{}\mRightarrow{} (\mforall{}x,y:\{x:\mBbbR{}| x \mmember{} [r0, r1]\} . ((x = y) {}\mRightarrow{} (g(x) = g(y))))
{}\mRightarrow{} (f(r1) = g(r0))
{}\mRightarrow{} (\mexists{}h:[r0, r1] {}\mrightarrow{}\mBbbR{}
((\mforall{}t:\{x:\mBbbR{}| x \mmember{} [r0, (r1/r(2))]\} . (h(t) = f(r(2) * t)))
\mwedge{} (\mforall{}t:\{x:\mBbbR{}| x \mmember{} [(r1/r(2)), r1]\} . (h(t) = g((r(2) * t) - r1)))
\mwedge{} (\mforall{}x,y:\{x:\mBbbR{}| x \mmember{} [r0, r1]\} . ((x = y) {}\mRightarrow{} (h(x) = h(y)))))))
Date html generated:
2020_05_20-PM-00_13_36
Last ObjectModification:
2020_01_08-AM-01_01_39
Theory : reals
Home
Index