---

Step * of Lemma convex-on_wf

∀[I:Interval]. ∀[f:I ⟶ℝ].  (convex-on(I;x.f[x]) ∈ ℙ)
BY
{ (ProveWfLemma THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. I : Interval
2. f : I ⟶ℝ
3. x : ℝ
4. y : ℝ
5. t : ℝ
6. x ∈ I
7. y ∈ I
8. r0 ≤ t
9. t ≤ r1
⊢ (t * x) + ((r1 - t) * y) ∈ I

---

Latex:

---

Latex:
\mforall{}[I:Interval].  \mforall{}[f:I  {}\mrightarrow{}\mBbbR{}].    (convex-on(I;x.f[x])  \mmember{}  \mBbbP{})


By

---

Latex:
(ProveWfLemma  THEN  MemTypeCD  THEN  Auto)

---

Home Index