---

Step * 1 of Lemma real-continuity2

.....antecedent..... 
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : [a, b] ⟶ℝ
5. real-sfun(f;a;b)
⊢ real-fun(f;a;b)
BY
{ (All (Unfolds ``real-sfun real-fun``) THEN RepeatFor 2 (ParallelLast')) }

1
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : [a, b] ⟶ℝ
5. x : {x:ℝ| x ∈ [a, b]} 
6. y : {x:ℝ| x ∈ [a, b]} 
7. f x ≠ f y ⇒ x ≠ y
⊢ (x = y) ⇒ ((f x) = (f y))

---

Latex:

---

Latex:
.....antecedent..... 
1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  a  \mleq{}  b
4.  f  :  [a,  b]  {}\mrightarrow{}\mBbbR{}
5.  real-sfun(f;a;b)
\mvdash{}  real-fun(f;a;b)


By

---

Latex:
(All  (Unfolds  ``real-sfun  real-fun``)  THEN  RepeatFor  2  (ParallelLast'))

---

Home Index