---

Step * of Lemma real-fun-iff-continuous

∀a,b:ℝ.  ∀f:[a, b] ⟶ℝ. (real-fun(f;a;b) ⇐⇒ real-cont(f;a;b)) supposing a ≤ b
BY
{ (InstLemma  `real-continuity` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Auto
   THEN D 0
   THEN Auto
   THEN InstLemma `continuous-rneq` [⌜[a, b]⌝;⌜λ2x.f x⌝]⋅
   THEN Auto) }

1
.....antecedent..... 
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : [a, b] ⟶ℝ
5. real-cont(f;a;b) supposing real-fun(f;a;b)
6. real-cont(f;a;b)
7. x : {x:ℝ| x ∈ [a, b]} 
8. y : {x:ℝ| x ∈ [a, b]} 
9. x = y
⊢ f x continuous for x ∈ [a, b]

2
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : [a, b] ⟶ℝ
5. real-cont(f;a;b) supposing real-fun(f;a;b)
6. real-cont(f;a;b)
7. x : {x:ℝ| x ∈ [a, b]} 
8. y : {x:ℝ| x ∈ [a, b]} 
9. x = y
10. ∀a@0,b:{x:ℝ| x ∈ [a, b]} .  (f a@0 ≠ f b ⇒ a@0 ≠ b)
⊢ (f x) = (f y)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.  (real-fun(f;a;b)  \mLeftarrow{}{}\mRightarrow{}  real-cont(f;a;b))  supposing  a  \mleq{}  b


By

---

Latex:
(InstLemma    `real-continuity`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  InstLemma  `continuous-rneq`  [\mkleeneopen{}[a,  b]\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.f  x\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index