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