---

Step * 1 1 1 1 of Lemma ifun-continuous


1. I : Interval
2. icompact(I)
3. f : {f:I ⟶ℝ| ifun(f;I)} 
4. I ~ [left-endpoint(I), right-endpoint(I)]
5. left-endpoint(I) ≤ right-endpoint(I)
6. ∀x,y:{x:ℝ| x ∈ [left-endpoint(I), right-endpoint(I)]} .  ((x = y) ⇒ ((f x) = (f y)))
⊢ ∀x,y:{x:ℝ| (left-endpoint(I) ≤ x) ∧ (x ≤ right-endpoint(I))} .  ((x = y) ⇒ ((f x) = (f y)))
BY
{ (Reduce -1 THEN Trivial) }

---

Latex:

---

Latex:

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


By

---

Latex:
(Reduce  -1  THEN  Trivial)

---

Home Index