---

Step * 1 of Lemma ifun-iff-continuous


1. I : Interval
2. icompact(I)
3. f : I ⟶ℝ
4. f[x] continuous for x ∈ I
⊢ ifun(λx.f[x];I)
BY
{ ((FLemma `icompact-is-rccint` [2] THENA Auto)
   THEN RWO "-1" 0
   THEN RWO "-1" (-2)
   THEN RWO "-1" (-3)
   THEN Reduce -1
   THEN RepUR ``ifun`` 0) }

1
1. I : Interval
2. icompact(I)
3. f : [left-endpoint(I), right-endpoint(I)] ⟶ℝ
4. f[x] continuous for x ∈ [left-endpoint(I), right-endpoint(I)]
5. I ~ [left-endpoint(I), right-endpoint(I)]
⊢ real-fun(λx.f[x];left-endpoint(I);right-endpoint(I))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  icompact(I)
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  f[x]  continuous  for  x  \mmember{}  I
\mvdash{}  ifun(\mlambda{}x.f[x];I)


By

---

Latex:
((FLemma  `icompact-is-rccint`  [2]  THENA  Auto)
  THEN  RWO  "-1"  0
  THEN  RWO  "-1"  (-2)
  THEN  RWO  "-1"  (-3)
  THEN  Reduce  -1
  THEN  RepUR  ``ifun``  0)

---

Home Index