---

Step * 1 of Lemma range-sup_wf


1. I : Interval
2. icompact(I)
3. f : I ⟶ℝ
4. mc : f x continuous for x ∈ I
⊢ TERMOF{sup-range:o, 1:l} I (λx.(f x)) ∈ λx.(f x)[x] continuous for x ∈ I ⟶ (∃y:ℝ. sup(λx.(f x)(x)(x∈I)) = y)
BY
{ xxxRepUR ``so_apply r-ap`` 0xxx }

1
1. I : Interval
2. icompact(I)
3. f : I ⟶ℝ
4. mc : f x continuous for x ∈ I
⊢ TERMOF{sup-range:o, 1:l} I (λx.(f x)) ∈ f x continuous for x ∈ I ⟶ (∃y:ℝ. sup(f x(x∈I)) = y)

---

Latex:

---

Latex:

1.  I  :  Interval
2.  icompact(I)
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  mc  :  f  x  continuous  for  x  \mmember{}  I
\mvdash{}  TERMOF\{sup-range:o,  1:l\}  I  (\mlambda{}x.(f  x))  \mmember{}  \mlambda{}x.(f  x)[x]  continuous  for  x  \mmember{}  I
    {}\mrightarrow{}  (\mexists{}y:\mBbbR{}.  sup(\mlambda{}x.(f  x)(x)(x\mmember{}I))  =  y)


By

---

Latex:
xxxRepUR  ``so\_apply  r-ap``  0xxx

---

Home Index