Step
*
1
1
1
1
2
of Lemma
real-path-comp-exists
1. f : [r0, r1] ⟶ℝ
2. g : [r0, r1] ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ [r0, r1]} . ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:{x:ℝ| x ∈ [r0, r1]} . ((x = y) ⇒ (g(x) = g(y)))
5. f(r1) = g(r0)
6. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (rmin(t;(r1/r(2))) = t)
7. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (r(2) * t ∈ [r0, r1])
8. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (f(r(2) * rmin(t;(r1/r(2)))) = f(r(2) * t))
9. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (rmax(t;(r1/r(2))) = t)
10. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . ((r(2) * t) - r1 ∈ [r0, r1])
11. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) = g((r(2) * t) - r1))
12. ∀t:{x:ℝ| x ∈ [r0, r1]} . (f(r(2) * rmin(t;(r1/r(2)))) ∈ ℝ)
13. ∀t:{x:ℝ| x ∈ [r0, r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) ∈ ℝ)
14. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
∃m:ℕ+
((|t - (r1/r(2))| ≤ (r1/r(m)))
⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(n))))
⊢ ∃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)))))
BY
{ (Assert ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
∃x:ℝ
(((t < ((r1/r(2)) + (r1/r(n)))) ∧ (x = f(r(2) * rmin(t;(r1/r(2))))))
∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ (x = g((r(2) * rmax(t;(r1/r(2)))) - r1)))) BY
(ParallelLast
THEN RepeatFor 2 ((D -5 With ⌜t⌝ THENA Auto))
THEN Auto
THEN (((InstLemma `rless-cases` [⌜(r1/r(2)) - (r1/r(n))⌝;⌜(r1/r(2)) + (r1/r(n))⌝;⌜t⌝]⋅
THENA (Auto THEN nRAdd ⌜(r1/r(n)) - (r1/r(2))⌝ 0⋅ THEN nRMul ⌜r(n)⌝ 0⋅ THEN Auto)
)
THEN D -1
THEN Auto)
THENL [(D 0 With ⌜g((r(2) * rmax(t;(r1/r(2)))) - r1)⌝ THEN Auto)
; (D 0 With ⌜f(r(2) * rmin(t;(r1/r(2))))⌝ THEN Auto)]
))) }
1
1. f : [r0, r1] ⟶ℝ
2. g : [r0, r1] ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ [r0, r1]} . ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:{x:ℝ| x ∈ [r0, r1]} . ((x = y) ⇒ (g(x) = g(y)))
5. f(r1) = g(r0)
6. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (rmin(t;(r1/r(2))) = t)
7. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (r(2) * t ∈ [r0, r1])
8. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (f(r(2) * rmin(t;(r1/r(2)))) = f(r(2) * t))
9. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (rmax(t;(r1/r(2))) = t)
10. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . ((r(2) * t) - r1 ∈ [r0, r1])
11. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) = g((r(2) * t) - r1))
12. ∀t:{x:ℝ| x ∈ [r0, r1]} . (f(r(2) * rmin(t;(r1/r(2)))) ∈ ℝ)
13. ∀t:{x:ℝ| x ∈ [r0, r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) ∈ ℝ)
14. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
∃m:ℕ+
((|t - (r1/r(2))| ≤ (r1/r(m)))
⇒ (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| ≤ (r1/r(n))))
15. ∀t:{x:ℝ| x ∈ [r0, r1]} . ∀n:ℕ+.
∃x:ℝ
(((t < ((r1/r(2)) + (r1/r(n)))) ∧ (x = f(r(2) * rmin(t;(r1/r(2))))))
∨ ((((r1/r(2)) - (r1/r(n))) < t) ∧ (x = g((r(2) * rmax(t;(r1/r(2)))) - r1))))
⊢ ∃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)))))
Latex:
Latex:
1. f : [r0, r1] {}\mrightarrow{}\mBbbR{}
2. g : [r0, r1] {}\mrightarrow{}\mBbbR{}
3. \mforall{}x,y:\{x:\mBbbR{}| x \mmember{} [r0, r1]\} . ((x = y) {}\mRightarrow{} (f(x) = f(y)))
4. \mforall{}x,y:\{x:\mBbbR{}| x \mmember{} [r0, r1]\} . ((x = y) {}\mRightarrow{} (g(x) = g(y)))
5. f(r1) = g(r0)
6. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [r0, (r1/r(2))]\} . (rmin(t;(r1/r(2))) = t)
7. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [r0, (r1/r(2))]\} . (r(2) * t \mmember{} [r0, r1])
8. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [r0, (r1/r(2))]\} . (f(r(2) * rmin(t;(r1/r(2)))) = f(r(2) * t))
9. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [(r1/r(2)), r1]\} . (rmax(t;(r1/r(2))) = t)
10. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [(r1/r(2)), r1]\} . ((r(2) * t) - r1 \mmember{} [r0, r1])
11. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [(r1/r(2)), r1]\} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) = g((r(2) * t) - r1))
12. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [r0, r1]\} . (f(r(2) * rmin(t;(r1/r(2)))) \mmember{} \mBbbR{})
13. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [r0, r1]\} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) \mmember{} \mBbbR{})
14. \mforall{}t:\{x:\mBbbR{}| x \mmember{} [r0, r1]\} . \mforall{}n:\mBbbN{}\msupplus{}.
\mexists{}m:\mBbbN{}\msupplus{}
((|t - (r1/r(2))| \mleq{} (r1/r(m)))
{}\mRightarrow{} (|f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1)| \mleq{} (r1/r(n))))
\mvdash{} \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)))))
By
Latex:
(Assert \mforall{}t:\{x:\mBbbR{}| x \mmember{} [r0, r1]\} . \mforall{}n:\mBbbN{}\msupplus{}.
\mexists{}x:\mBbbR{}
(((t < ((r1/r(2)) + (r1/r(n)))) \mwedge{} (x = f(r(2) * rmin(t;(r1/r(2))))))
\mvee{} ((((r1/r(2)) - (r1/r(n))) < t) \mwedge{} (x = g((r(2) * rmax(t;(r1/r(2)))) - r1)))) BY
(ParallelLast
THEN RepeatFor 2 ((D -5 With \mkleeneopen{}t\mkleeneclose{} THENA Auto))
THEN Auto
THEN (((InstLemma `rless-cases` [\mkleeneopen{}(r1/r(2)) - (r1/r(n))\mkleeneclose{};\mkleeneopen{}(r1/r(2)) + (r1/r(n))\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{}]\mcdot{}
THENA (Auto THEN nRAdd \mkleeneopen{}(r1/r(n)) - (r1/r(2))\mkleeneclose{} 0\mcdot{} THEN nRMul \mkleeneopen{}r(n)\mkleeneclose{} 0\mcdot{} THEN Auto)
)
THEN D -1
THEN Auto)
THENL [(D 0 With \mkleeneopen{}g((r(2) * rmax(t;(r1/r(2)))) - r1)\mkleeneclose{} THEN Auto)
; (D 0 With \mkleeneopen{}f(r(2) * rmin(t;(r1/r(2))))\mkleeneclose{} THEN Auto)]
)))
Home
Index