---

Step * 1 of Lemma rmin-lb-convex


1. a : ℝ
2. b : ℝ
3. t : ℝ
4. r0 ≤ t
5. t ≤ r1
⊢ rmin(a;b) ≤ ((t * a) + ((r1 - t) * b))
BY
{ ((Assert (t * rmin(a;b)) ≤ (t * a) BY
          ((Assert rmin(a;b) ≤ a BY Auto) THEN nRMul ⌜t⌝ (-1)⋅ THEN Auto))
   THEN (Assert ((r1 - t) * rmin(a;b)) ≤ ((r1 - t) * b) BY
               ((Assert rmin(a;b) ≤ b BY Auto) THEN nRMul ⌜r1 - t⌝ (-1)⋅ THEN Auto))
   THEN RWO "-1< -2<" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  t  :  \mBbbR{}
4.  r0  \mleq{}  t
5.  t  \mleq{}  r1
\mvdash{}  rmin(a;b)  \mleq{}  ((t  *  a)  +  ((r1  -  t)  *  b))


By

---

Latex:
((Assert  (t  *  rmin(a;b))  \mleq{}  (t  *  a)  BY
                ((Assert  rmin(a;b)  \mleq{}  a  BY  Auto)  THEN  nRMul  \mkleeneopen{}t\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto))
  THEN  (Assert  ((r1  -  t)  *  rmin(a;b))  \mleq{}  ((r1  -  t)  *  b)  BY
                          ((Assert  rmin(a;b)  \mleq{}  b  BY  Auto)  THEN  nRMul  \mkleeneopen{}r1  -  t\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto))
  THEN  RWO  "-1<  -2<"  0
  THEN  Auto)

---

Home Index