---

Step * 1 of Lemma ifun_wf


1. I : Interval
2. f : I ⟶ℝ
3. icompact(I)
⊢ f ∈ [left-endpoint(I), right-endpoint(I)] ⟶ℝ
BY
{ ((FLemma `icompact-is-rccint` [-1] THENA Auto) THEN RWO "-1<" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  icompact(I)
\mvdash{}  f  \mmember{}  [left-endpoint(I),  right-endpoint(I)]  {}\mrightarrow{}\mBbbR{}


By

---

Latex:
((FLemma  `icompact-is-rccint`  [-1]  THENA  Auto)  THEN  RWO  "-1<"  0  THEN  Auto)

---

Home Index