---

Step * 1 of Lemma range-inf-property


1. I : {I:Interval| icompact(I)} 
2. f : I ⟶ℝ
3. mc : f x continuous for x ∈ I
4. v : ∀f:I ⟶ℝ. (f[x] continuous for x ∈ I ⇒ (∃y:ℝ. inf(f(x)(x∈I)) = y))
5. (TERMOF{inf-range:o, 1:l} I) = v ∈ (∀f:I ⟶ℝ. (f[x] continuous for x ∈ I ⇒ (∃y:ℝ. inf(f(x)(x∈I)) = y)))
⊢ inf(f x(x∈I)) = fst((v (λx.(f x)) mc))
BY
{ (RepUR ``so_apply r-ap`` -2 THEN Auto)⋅ }

1
1. I : {I:Interval| icompact(I)} 
2. f : I ⟶ℝ
3. mc : f x continuous for x ∈ I
4. v : ∀f:I ⟶ℝ. (f x continuous for x ∈ I ⇒ (∃y:ℝ. inf(f x(x∈I)) = y))
5. (TERMOF{inf-range:o, 1:l} I) = v ∈ (∀f:I ⟶ℝ. (f[x] continuous for x ∈ I ⇒ (∃y:ℝ. inf(f(x)(x∈I)) = y)))
⊢ inf(f x(x∈I)) = fst((v (λx.(f x)) mc))

---

Latex:

---

Latex:

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


By

---

Latex:
(RepUR  ``so\_apply  r-ap``  -2  THEN  Auto)\mcdot{}

---

Home Index