---

Step * of Lemma range-inf_wf

∀[I:{I:Interval| icompact(I)} ]. ∀[f:I ⟶ℝ]. ∀[mc:f[x] continuous for x ∈ I].  (inf{f[x]|x ∈ I} ∈ ℝ)
BY
{ xxxxxx(All (Unfold `so_apply`) THEN ProveWfLemma)xxxxxx }

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

---

Latex:

---

Latex:
\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\}  \mmember{}  \mBbbR{})


By

---

Latex:
xxxxxx(All  (Unfold  `so\_apply`)  THEN  ProveWfLemma)xxxxxx

---

Home Index