Step
*
1
2
1
of Lemma
concave-positive-nonzero-on
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))}
7. i-approx(I;m) ⊆ I
8. left-endpoint(i-approx(I;m)) ∈ I
9. right-endpoint(i-approx(I;m)) ∈ I
10. r0 < rmin(f[left-endpoint(i-approx(I;m))];f[right-endpoint(i-approx(I;m))])
11. x : ℝ
12. x ∈ i-approx(I;m)
13. r0 < f[x]
⊢ rmin(f[left-endpoint(i-approx(I;m))];f[right-endpoint(i-approx(I;m))]) ≤ f[x]
BY
{ (StableCases ⌜left-endpoint(i-approx(I;m)) < right-endpoint(i-approx(I;m))⌝⋅ THENA Auto) }
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))}
7. i-approx(I;m) ⊆ I
8. left-endpoint(i-approx(I;m)) ∈ I
9. right-endpoint(i-approx(I;m)) ∈ I
10. r0 < rmin(f[left-endpoint(i-approx(I;m))];f[right-endpoint(i-approx(I;m))])
11. x : ℝ
12. x ∈ i-approx(I;m)
13. r0 < f[x]
14. left-endpoint(i-approx(I;m)) < right-endpoint(i-approx(I;m))
⊢ rmin(f[left-endpoint(i-approx(I;m))];f[right-endpoint(i-approx(I;m))]) ≤ f[x]
2
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))}
7. i-approx(I;m) ⊆ I
8. left-endpoint(i-approx(I;m)) ∈ I
9. right-endpoint(i-approx(I;m)) ∈ I
10. r0 < rmin(f[left-endpoint(i-approx(I;m))];f[right-endpoint(i-approx(I;m))])
11. x : ℝ
12. x ∈ i-approx(I;m)
13. r0 < f[x]
14. ¬(left-endpoint(i-approx(I;m)) < right-endpoint(i-approx(I;m)))
⊢ rmin(f[left-endpoint(i-approx(I;m))];f[right-endpoint(i-approx(I;m))]) ≤ f[x]
Latex:
Latex:
1. I : Interval
2. f : I {}\mrightarrow{}\mBbbR{}
3. \mforall{}x,y:\mBbbR{}. ((x \mmember{} I) {}\mRightarrow{} (y \mmember{} I) {}\mRightarrow{} (x = y) {}\mRightarrow{} (f[x] = f[y]))
4. \mforall{}x:\mBbbR{}. ((x \mmember{} I) {}\mRightarrow{} (r0 < f[x]))
5. concave-on(I;x.f[x])
6. m : \{m:\mBbbN{}\msupplus{}| icompact(i-approx(I;m))\}
7. i-approx(I;m) \msubseteq{} I
8. left-endpoint(i-approx(I;m)) \mmember{} I
9. right-endpoint(i-approx(I;m)) \mmember{} I
10. r0 < rmin(f[left-endpoint(i-approx(I;m))];f[right-endpoint(i-approx(I;m))])
11. x : \mBbbR{}
12. x \mmember{} i-approx(I;m)
13. r0 < f[x]
\mvdash{} rmin(f[left-endpoint(i-approx(I;m))];f[right-endpoint(i-approx(I;m))]) \mleq{} f[x]
By
Latex:
(StableCases \mkleeneopen{}left-endpoint(i-approx(I;m)) < right-endpoint(i-approx(I;m))\mkleeneclose{}\mcdot{} THENA Auto)
Home
Index