---

Step * 1 1 1 1 1 of Lemma general-partition-sum-no-mc

.....wf..... 
1. I : Interval
2. icompact(I)
3. f : {f:I ⟶ℝ| ifun(f;I)} 
4. I ~ [left-endpoint(I), right-endpoint(I)]
5. real-fun(f;left-endpoint(I);right-endpoint(I))
⊢ right-endpoint(I) ∈ {b:ℝ| left-endpoint(I) ≤ b} 
BY
{ (MemTypeCD THEN EAuto 1) }

---

Latex:

---

Latex:
.....wf..... 
1.  I  :  Interval
2.  icompact(I)
3.  f  :  \{f:I  {}\mrightarrow{}\mBbbR{}|  ifun(f;I)\} 
4.  I  \msim{}  [left-endpoint(I),  right-endpoint(I)]
5.  real-fun(f;left-endpoint(I);right-endpoint(I))
\mvdash{}  right-endpoint(I)  \mmember{}  \{b:\mBbbR{}|  left-endpoint(I)  \mleq{}  b\} 


By

---

Latex:
(MemTypeCD  THEN  EAuto  1)

---

Home Index