---

Step * of Lemma i-member-convex

∀I:Interval. ∀a,b:ℝ.  ((a ∈ I) ⇒ (b ∈ I) ⇒ (∀t:ℝ. ((r0 ≤ t) ⇒ (t ≤ r1) ⇒ ((t * a) + ((r1 - t) * b) ∈ I))))
BY
{ (Auto THEN Using [`a',⌜rmin(a;b)⌝;`b',⌜rmax(a;b)⌝] (BLemma `i-member-between` )⋅ THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}a,b:\mBbbR{}.
    ((a  \mmember{}  I)  {}\mRightarrow{}  (b  \mmember{}  I)  {}\mRightarrow{}  (\mforall{}t:\mBbbR{}.  ((r0  \mleq{}  t)  {}\mRightarrow{}  (t  \mleq{}  r1)  {}\mRightarrow{}  ((t  *  a)  +  ((r1  -  t)  *  b)  \mmember{}  I))))


By

---

Latex:
(Auto  THEN  Using  [`a',\mkleeneopen{}rmin(a;b)\mkleeneclose{};`b',\mkleeneopen{}rmax(a;b)\mkleeneclose{}]  (BLemma  `i-member-between`  )\mcdot{}  THEN  EAuto  1)

---

Home Index