---

Step * of Lemma ifun-continuous

∀I:Interval. (icompact(I) ⇒ (∀f:{f:I ⟶ℝ| ifun(f;I)} . f[x] continuous for x ∈ I))
BY
{ (Auto THEN (FLemma `icompact-is-rccint` [2] THENA Auto)) }

1
1. I : Interval
2. icompact(I)
3. f : {f:I ⟶ℝ| ifun(f;I)} 
4. I ~ [left-endpoint(I), right-endpoint(I)]
⊢ f[x] continuous for x ∈ I

---

Latex:

---

Latex:
\mforall{}I:Interval.  (icompact(I)  {}\mRightarrow{}  (\mforall{}f:\{f:I  {}\mrightarrow{}\mBbbR{}|  ifun(f;I)\}  .  f[x]  continuous  for  x  \mmember{}  I))


By

---

Latex:
(Auto  THEN  (FLemma  `icompact-is-rccint`  [2]  THENA  Auto))

---

Home Index