Step
*
of Lemma
concave-positive-nonzero-on
∀I:Interval. ∀f:I ⟶ℝ.
((∀x,y:ℝ. ((x ∈ I)
⇒ (y ∈ I)
⇒ (x = y)
⇒ (f[x] = f[y])))
⇒ (∀x:ℝ. ((x ∈ I)
⇒ (r0 < f[x])))
⇒ concave-on(I;x.f[x])
⇒ f[x]≠r0 for x ∈ I)
BY
{ xxx(Auto THEN D 0 THEN Auto)xxx }
1
1. I : Interval
2. f : I ⟶ℝ
3. ∀x,y:ℝ. ((x ∈ I)
⇒ (y ∈ I)
⇒ (x = y)
⇒ (f[x] = f[y]))
4. ∀x:ℝ. ((x ∈ I)
⇒ (r0 < f[x]))
5. concave-on(I;x.f[x])
6. m : {m:ℕ+| icompact(i-approx(I;m))}
⊢ ∃c:ℝ [((r0 < c) ∧ (∀x:ℝ. ((x ∈ i-approx(I;m))
⇒ (c ≤ |f[x]|))))]
Latex:
Latex:
\mforall{}I:Interval. \mforall{}f:I {}\mrightarrow{}\mBbbR{}.
((\mforall{}x,y:\mBbbR{}. ((x \mmember{} I) {}\mRightarrow{} (y \mmember{} I) {}\mRightarrow{} (x = y) {}\mRightarrow{} (f[x] = f[y])))
{}\mRightarrow{} (\mforall{}x:\mBbbR{}. ((x \mmember{} I) {}\mRightarrow{} (r0 < f[x])))
{}\mRightarrow{} concave-on(I;x.f[x])
{}\mRightarrow{} f[x]\mneq{}r0 for x \mmember{} I)
By
Latex:
xxx(Auto THEN D 0 THEN Auto)xxx
Home
Index