---

Step * 1 1 of Lemma ifun-iff-continuous


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))
BY
{ (BLemma `real-fun-iff-continuous` THEN Auto) }

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)]
⊢ left-endpoint(I) ≤ right-endpoint(I)

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

---

Latex:

---

Latex:

1.  I  :  Interval
2.  icompact(I)
3.  f  :  [left-endpoint(I),  right-endpoint(I)]  {}\mrightarrow{}\mBbbR{}
4.  f[x]  continuous  for  x  \mmember{}  [left-endpoint(I),  right-endpoint(I)]
5.  I  \msim{}  [left-endpoint(I),  right-endpoint(I)]
\mvdash{}  real-fun(\mlambda{}x.f[x];left-endpoint(I);right-endpoint(I))


By

---

Latex:
(BLemma  `real-fun-iff-continuous`  THEN  Auto)

---

Home Index