---

Step * 1 of Lemma path-comp-for-reals

.....wf..... 
1. f : {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ ℝ| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  ((¬t ≠ t') ⇒ (¬f t ≠ f t'))} 
2. g : {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ ℝ| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  ((¬t ≠ t') ⇒ (¬f t ≠ f t'))} 
3. ¬f@r1 ≠ g@r0
4. h : [r0, r1] ⟶ℝ
5. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (h(t) = f(r(2) * t))
6. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (h(t) = g((r(2) * t) - r1))
7. ∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) ⇒ (h(x) = h(y)))
⊢ h ∈ {f:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  ⟶ ℝ| ∀t,t':{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  ((¬t ≠ t') ⇒ (¬f t ≠ f t'))} 
BY
{ (MemTypeCD
   THEN Auto
   THEN (Assert h(t) = h(t') BY
               (BackThruSomeHyp THEN EAuto 1))
   THEN Fold `r-ap` 0
   THEN RWO  "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  f  :  \{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  \mBbbR{}| 
                \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    ((\mneg{}t  \mneq{}  t')  {}\mRightarrow{}  (\mneg{}f  t  \mneq{}  f  t'))\} 
2.  g  :  \{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  \mBbbR{}| 
                \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    ((\mneg{}t  \mneq{}  t')  {}\mRightarrow{}  (\mneg{}f  t  \mneq{}  f  t'))\} 
3.  \mneg{}f@r1  \mneq{}  g@r0
4.  h  :  [r0,  r1]  {}\mrightarrow{}\mBbbR{}
5.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  (r1/r(2))]\}  .  (h(t)  =  f(r(2)  *  t))
6.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [(r1/r(2)),  r1]\}  .  (h(t)  =  g((r(2)  *  t)  -  r1))
7.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}  .    ((x  =  y)  {}\mRightarrow{}  (h(x)  =  h(y)))
\mvdash{}  h  \mmember{}  \{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  \mBbbR{}| 
              \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    ((\mneg{}t  \mneq{}  t')  {}\mRightarrow{}  (\mneg{}f  t  \mneq{}  f  t'))\} 


By

---

Latex:
(MemTypeCD
  THEN  Auto
  THEN  (Assert  h(t)  =  h(t')  BY
                          (BackThruSomeHyp  THEN  EAuto  1))
  THEN  Fold  `r-ap`  0
  THEN  RWO    "-1"  0
  THEN  Auto)

---

Home Index