Step
*
2
2
of Lemma
path-comp-for-reals
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:ℝ| (r0 ≤ x) ∧ (x ≤ (r1/r(2)))} . ((h t) = (f (r(2) * t)))
6. ∀t:{x:ℝ| ((r1/r(2)) ≤ x) ∧ (x ≤ r1)} . ((h t) = (g ((r(2) * t) - r1)))
7. ∀x,y:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  ((x = y) 
⇒ ((h x) = (h y)))
⊢ ∀t:{x:ℝ| ((r1/r(2)) ≤ x) ∧ (x ≤ r1)} . (¬h t ≠ g ((r(2) * t) - r1))
BY
{ ParallelLast }
1
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:ℝ| (r0 ≤ x) ∧ (x ≤ (r1/r(2)))} . ((h t) = (f (r(2) * t)))
6. ∀t:{x:ℝ| ((r1/r(2)) ≤ x) ∧ (x ≤ r1)} . ((h t) = (g ((r(2) * t) - r1)))
7. ∀x,y:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  ((x = y) 
⇒ ((h x) = (h y)))
8. t : {x:ℝ| ((r1/r(2)) ≤ x) ∧ (x ≤ r1)} 
9. ∀y:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} . ((t = y) 
⇒ ((h t) = (h y)))
⊢ ¬h t ≠ g ((r(2) * t) - r1)
Latex:
Latex:
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{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  (r1/r(2)))\}  .  ((h  t)  =  (f  (r(2)  *  t)))
6.  \mforall{}t:\{x:\mBbbR{}|  ((r1/r(2))  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .  ((h  t)  =  (g  ((r(2)  *  t)  -  r1)))
7.  \mforall{}x,y:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    ((x  =  y)  {}\mRightarrow{}  ((h  x)  =  (h  y)))
\mvdash{}  \mforall{}t:\{x:\mBbbR{}|  ((r1/r(2))  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .  (\mneg{}h  t  \mneq{}  g  ((r(2)  *  t)  -  r1))
By
Latex:
ParallelLast
Home
Index