---

Step * of Lemma implies-convex-on

∀[I:Interval]. ∀[f:I ⟶ℝ].
  ((∀x,y:ℝ.  ((x ∈ I) ⇒ (y ∈ I) ⇒ (x = y) ⇒ (f[x] = f[y])))
  ⇒ (∀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])))))))
  ⇒ convex-on(I;x.f[x]))
BY
{ (Auto
   THEN Try (MemTypeCD)
   THEN Try (BLemma `i-member-convex`)
   THEN Auto
   THEN (D 0 THEN Auto)
   THEN (Assert (t * x) + ((r1 - t) * y) ∈ I BY
               (BLemma `i-member-convex` 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
⊢ f[(t * x) + ((r1 - t) * y)] ≤ ((t * f[x]) + ((r1 - t) * f[y]))

---

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,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])))))))
    {}\mRightarrow{}  convex-on(I;x.f[x]))


By

---

Latex:
(Auto
  THEN  Try  (MemTypeCD)
  THEN  Try  (BLemma  `i-member-convex`)
  THEN  Auto
  THEN  (D  0  THEN  Auto)
  THEN  (Assert  (t  *  x)  +  ((r1  -  t)  *  y)  \mmember{}  I  BY
                          (BLemma  `i-member-convex`  THEN  Auto)))

---

Home Index