---

Step * 1 2 1 of Lemma implies-convex-on


1. I : Interval
2. f : I ⟶ℝ
3. ∀x,y:ℝ.  ((x ∈ I) ⇒ (y ∈ I) ⇒ (x = y) ⇒ (f[x] = f[y]))
4. ∀x,y:ℝ.
     ((x < y)
     ⇒ (∀t:ℝ
           ((x ∈ I) ⇒ (y ∈ I) ⇒ (t ∈ [r0, r1]) ⇒ (f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))))))
5. x : ℝ
6. y : ℝ
7. t : ℝ
8. x ∈ I
9. y ∈ I
10. t ∈ [r0, r1]
11. (t * x) + ((r1 - t) * y) ∈ I
12. ¬(x < y)
13. ¬(y < x)
14. x = y
⊢ f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))
BY
{ ((Assert f[x] = f[y] BY Auto) THEN (Assert ((t * x) + ((r1 - t) * y)) = y BY (RWO "-2" 0 THEN Auto))) }

1
1. I : Interval
2. f : I ⟶ℝ
3. ∀x,y:ℝ.  ((x ∈ I) ⇒ (y ∈ I) ⇒ (x = y) ⇒ (f[x] = f[y]))
4. ∀x,y:ℝ.
     ((x < y)
     ⇒ (∀t:ℝ
           ((x ∈ I) ⇒ (y ∈ I) ⇒ (t ∈ [r0, r1]) ⇒ (f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))))))
5. x : ℝ
6. y : ℝ
7. t : ℝ
8. x ∈ I
9. y ∈ I
10. t ∈ [r0, r1]
11. (t * x) + ((r1 - t) * y) ∈ I
12. ¬(x < y)
13. ¬(y < x)
14. x = y
15. f[x] = f[y]
16. ((t * x) + ((r1 - t) * y)) = y
⊢ f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))

---

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,y:\mBbbR{}.
          ((x  <  y)
          {}\mRightarrow{}  (\mforall{}t:\mBbbR{}
                      ((x  \mmember{}  I)
                      {}\mRightarrow{}  (y  \mmember{}  I)
                      {}\mRightarrow{}  (t  \mmember{}  [r0,  r1])
                      {}\mRightarrow{}  (f[(t  *  x)  +  ((r1  -  t)  *  y)]  \mleq{}  ((t  *  f[x])  +  ((r1  -  t)  *  f[y]))))))
5.  x  :  \mBbbR{}
6.  y  :  \mBbbR{}
7.  t  :  \mBbbR{}
8.  x  \mmember{}  I
9.  y  \mmember{}  I
10.  t  \mmember{}  [r0,  r1]
11.  (t  *  x)  +  ((r1  -  t)  *  y)  \mmember{}  I
12.  \mneg{}(x  <  y)
13.  \mneg{}(y  <  x)
14.  x  =  y
\mvdash{}  f[(t  *  x)  +  ((r1  -  t)  *  y)]  \mleq{}  ((t  *  f[x])  +  ((r1  -  t)  *  f[y]))


By

---

Latex:
((Assert  f[x]  =  f[y]  BY
                Auto)
  THEN  (Assert  ((t  *  x)  +  ((r1  -  t)  *  y))  =  y  BY
                          (RWO  "-2"  0  THEN  Auto))
  )

---

Home Index