---

Step * 1 of Lemma ifun-alt


1. I : Interval
2. [f] : I ⟶ℝ
3. [%] : icompact(I)
4. [%1] : ∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ (f(x) = f(y)))
5. x : {x:ℝ| x ∈ [left-endpoint(I), right-endpoint(I)]} 
6. y : {x:ℝ| x ∈ [left-endpoint(I), right-endpoint(I)]} 
7. x = y
⊢ (f x) = (f y)
BY
{ ((Assert icompact(I) BY
          (Unhide THEN Auto))
   THEN (Assert [left-endpoint(I), right-endpoint(I)] ⊆ I  BY
               EAuto 1)
   THEN Fold `r-ap` 0
   THEN (Assert x ∈ I BY
               EAuto 1)
   THEN (Assert y ∈ I BY
               EAuto 1)
   THEN Unhide
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  [f]  :  I  {}\mrightarrow{}\mBbbR{}
3.  [\%]  :  icompact(I)
4.  [\%1]  :  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y)))
5.  x  :  \{x:\mBbbR{}|  x  \mmember{}  [left-endpoint(I),  right-endpoint(I)]\} 
6.  y  :  \{x:\mBbbR{}|  x  \mmember{}  [left-endpoint(I),  right-endpoint(I)]\} 
7.  x  =  y
\mvdash{}  (f  x)  =  (f  y)


By

---

Latex:
((Assert  icompact(I)  BY
                (Unhide  THEN  Auto))
  THEN  (Assert  [left-endpoint(I),  right-endpoint(I)]  \msubseteq{}  I    BY
                          EAuto  1)
  THEN  Fold  `r-ap`  0
  THEN  (Assert  x  \mmember{}  I  BY
                          EAuto  1)
  THEN  (Assert  y  \mmember{}  I  BY
                          EAuto  1)
  THEN  Unhide
  THEN  Auto)

---

Home Index