---

Step * of Lemma ifun_wf

∀[I:Interval]. ∀[f:I ⟶ℝ].  ifun(f;I) ∈ ℙ supposing icompact(I)
BY
{ ProveWfLemma }

1
1. I : Interval
2. f : I ⟶ℝ
3. icompact(I)
⊢ f ∈ [left-endpoint(I), right-endpoint(I)] ⟶ℝ

---

Latex:

---

Latex:
\mforall{}[I:Interval].  \mforall{}[f:I  {}\mrightarrow{}\mBbbR{}].    ifun(f;I)  \mmember{}  \mBbbP{}  supposing  icompact(I)


By

---

Latex:
ProveWfLemma

---

Home Index