---

Step * 1 1 1 of Lemma Riemann-integral-rless


1. a : ℝ
2. b : {b:ℝ| a < b} 
3. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
4. c : ℝ
5. ∀x:ℝ. ((x ∈ [a, b]) ⇒ (f[x] ≤ c))
6. x : ℝ
7. x ∈ [a, b]
8. f[x] < c
9. a < b
10. x1 : {t:ℝ| t ∈ [a, b]} 
11. y : {t:ℝ| t ∈ [a, b]} 
12. x1 = y
⊢ f[x1] = f[y]
BY
{ (DVar `f' THEN Unhide THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \{b:\mBbbR{}|  a  <  b\} 
3.  f  :  \{f:[a,  b]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[a,  b])\} 
4.  c  :  \mBbbR{}
5.  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  [a,  b])  {}\mRightarrow{}  (f[x]  \mleq{}  c))
6.  x  :  \mBbbR{}
7.  x  \mmember{}  [a,  b]
8.  f[x]  <  c
9.  a  <  b
10.  x1  :  \{t:\mBbbR{}|  t  \mmember{}  [a,  b]\} 
11.  y  :  \{t:\mBbbR{}|  t  \mmember{}  [a,  b]\} 
12.  x1  =  y
\mvdash{}  f[x1]  =  f[y]


By

---

Latex:
(DVar  `f'  THEN  Unhide  THEN  Auto)

---

Home Index