---

Step * of Lemma inf-range-no-mc

∀I:{I:Interval| icompact(I)} . ∀f:{f:I ⟶ℝ| ifun(f;I)} .  ∃y:ℝ. inf(f(x)(x∈I)) = y
BY
{ ((Auto THEN BLemma `inf-range` THEN Auto) THEN InstLemma `ifun-continuous` [⌜I⌝;⌜f⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I:\{I:Interval|  icompact(I)\}  .  \mforall{}f:\{f:I  {}\mrightarrow{}\mBbbR{}|  ifun(f;I)\}  .    \mexists{}y:\mBbbR{}.  inf(f(x)(x\mmember{}I))  =  y


By

---

Latex:
((Auto  THEN  BLemma  `inf-range`  THEN  Auto)  THEN  InstLemma  `ifun-continuous`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index