---

Step * of Lemma range-inf-property

No Annotations
∀I:{I:Interval| icompact(I)} . ∀f:I ⟶ℝ. ∀mc:f[x] continuous for x ∈ I.  inf(f[x](x∈I)) = inf{f[x]|x ∈ I}
BY
{ (TACTIC:(All (Unfold `so_apply`) THEN Auto) THEN Unfold `range-inf` 0 THEN GenConclAtAddr [2;1;1;1] ) }

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:
No  Annotations
\mforall{}I:\{I:Interval|  icompact(I)\}  .  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.  \mforall{}mc:f[x]  continuous  for  x  \mmember{}  I.
    inf(f[x](x\mmember{}I))  =  inf\{f[x]|x  \mmember{}  I\}


By

---

Latex:
(TACTIC:(All  (Unfold  `so\_apply`)  THEN  Auto)
  THEN  Unfold  `range-inf`  0
  THEN  GenConclAtAddr  [2;1;1;1]  )

---

Home Index