---

Step * of Lemma ifun-alt

∀I:Interval. ∀[f:I ⟶ℝ]. (ifun(f;I)) supposing ((∀x,y:{x:ℝ| x ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))) and icompact(I))
BY
{ ((Fold `r-ap` 0 THEN Intros) THEN RepeatFor 3 ((D 0 THENA Auto))) }

1
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)

---

Latex:

---

Latex:
\mforall{}I:Interval
    \mforall{}[f:I  {}\mrightarrow{}\mBbbR{}]
        (ifun(f;I))  supposing  ((\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y))))  and  icompact(I))


By

---

Latex:
((Fold  `r-ap`  0  THEN  Intros)  THEN  RepeatFor  3  ((D  0  THENA  Auto)))

---

Home Index