---

Step * 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)]
⊢ f[x] continuous for x ∈ I
BY
{ (RWO "-1" 0
   THEN (Assert left-endpoint(I) ≤ right-endpoint(I) BY
               (RepeatFor 2 (D 2) THEN RWO "-1" 3 THEN Reduce 3 THEN Auto))
   THEN (BLemma  `real-cont-iff-continuous` THENA Auto)
   THEN Try ((RelRST THEN Auto))) }

1
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)
⊢ real-cont(λ2x.f[x];left-endpoint(I);right-endpoint(I))

---

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)]
\mvdash{}  f[x]  continuous  for  x  \mmember{}  I


By

---

Latex:
(RWO  "-1"  0
  THEN  (Assert  left-endpoint(I)  \mleq{}  right-endpoint(I)  BY
                          (RepeatFor  2  (D  2)  THEN  RWO  "-1"  3  THEN  Reduce  3  THEN  Auto))
  THEN  (BLemma    `real-cont-iff-continuous`  THENA  Auto)
  THEN  Try  ((RelRST  THEN  Auto)))

---

Home Index