---

Step * of Lemma partition-sum_wf

∀I:Interval
  (icompact(I)
  ⇒ (∀p:partition(I). ∀f:I ⟶ℝ. ∀x:partition-choice(full-partition(I;p)).
        (partition-sum(f;x;full-partition(I;p)) ∈ ℝ)))
BY
{ (ProveWfLemma THEN BLemma `partition-choice-member` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}I:Interval
    (icompact(I)
    {}\mRightarrow{}  (\mforall{}p:partition(I).  \mforall{}f:I  {}\mrightarrow{}\mBbbR{}.  \mforall{}x:partition-choice(full-partition(I;p)).
                (partition-sum(f;x;full-partition(I;p))  \mmember{}  \mBbbR{})))


By

---

Latex:
(ProveWfLemma  THEN  BLemma  `partition-choice-member`  THEN  Auto)

---

Home Index