Step
*
of Lemma
range_inf-bound
No Annotations
∀I:{I:Interval| icompact(I)} . ∀f:{x:ℝ| x ∈ I} ⟶ ℝ.
∀[c:ℝ]. c ≤ inf{f[x] | x ∈ I} supposing ∀x:ℝ. ((x ∈ I)
⇒ (c ≤ f[x]))
supposing ∀x,y:{x:ℝ| x ∈ I} . ((x = y)
⇒ (f[x] = f[y]))
BY
{ (InstLemma `range_inf-property` []
THEN RepeatFor 3 (ParallelLast')
THEN MoveToConcl (-1)
THEN GenConcl ⌜inf{f[x] | x ∈ I} = s ∈ ℝ⌝⋅
THEN Auto) }
1
1. I : {I:Interval| icompact(I)}
2. f : {x:ℝ| x ∈ I} ⟶ ℝ
3. ∀x,y:{x:ℝ| x ∈ I} . ((x = y)
⇒ (f[x] = f[y]))
4. s : ℝ
5. inf{f[x] | x ∈ I} = s ∈ ℝ
6. inf(f[x](x∈I)) = s
7. c : ℝ
8. ∀x:ℝ. ((x ∈ I)
⇒ (c ≤ f[x]))
⊢ c ≤ s
Latex:
Latex:
No Annotations
\mforall{}I:\{I:Interval| icompact(I)\} . \mforall{}f:\{x:\mBbbR{}| x \mmember{} I\} {}\mrightarrow{} \mBbbR{}.
\mforall{}[c:\mBbbR{}]. c \mleq{} inf\{f[x] | x \mmember{} I\} supposing \mforall{}x:\mBbbR{}. ((x \mmember{} I) {}\mRightarrow{} (c \mleq{} f[x]))
supposing \mforall{}x,y:\{x:\mBbbR{}| x \mmember{} I\} . ((x = y) {}\mRightarrow{} (f[x] = f[y]))
By
Latex:
(InstLemma `range\_inf-property` []
THEN RepeatFor 3 (ParallelLast')
THEN MoveToConcl (-1)
THEN GenConcl \mkleeneopen{}inf\{f[x] | x \mmember{} I\} = s\mkleeneclose{}\mcdot{}
THEN Auto)
Home
Index